theorem :: ZF_LANG1:84

for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is being_equality holds
( M,v |= H iff v . (Var1 H) = v . (Var2 H) )