theorem :: ZF_MODEL:11

for H being ZF-formula
for E being non empty set st H is universal holds
for f being Function of VAR,E holds
( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St ((the_scope_of H),E) ) ) iff f in St (H,E) )