theorem :: ZF_MODEL:8

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