theorem :: ZF_MODEL:7

for H being ZF-formula
for E being non empty set st H is being_equality holds
for f being Function of VAR,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) )