theorem :: ZF_MODEL:21

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