theorem Th20: :: ZF_MODEL:20

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