theorem Th6: :: ZF_MODEL:6

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