theorem :: ZF_LANG1:75

for H being ZF-formula
for M being non empty set
for v, v9 being Function of VAR,M st ( for x being Variable st x in Free H holds
v9 . x = v . x ) & M,v |= H holds
M,v9 |= H