theorem :: ZF_MODEL:22

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 |= Ex (x,y,H) iff ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )