let E be non empty set ; :: thesis: 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 ) )
let f be Function of VAR ,E; :: thesis: 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 ) )
let H be ZF-formula; :: thesis: 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 ) )
let x be Variable; :: thesis: ( 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 ) )
A1: ( E,f |= 'not' (All x,('not' H)) iff not E,f |= All x,('not' H) ) by Th14;
thus ( E,f |= Ex x,H implies ex g being Function of VAR ,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) ) :: thesis: ( ex g being Function of VAR ,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) implies E,f |= Ex x,H )

proof

assume E,f |= Ex x,H ; :: thesis: ex g being Function of VAR ,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H )
then consider g being Function of VAR ,E such that
A2: for y being Variable st g . y <> f . y holds
x = y and
A3: not E,g |= 'not' H by A1, Th16;
E,g |= H by A3, Th14;
hence ex g being Function of VAR ,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) by A2; :: thesis: verum

end;

given g being Function of VAR ,E such that A4: for y being Variable st g . y <> f . y holds
x = y and
A5: E,g |= H ; :: thesis: E,f |= Ex x,H
not E,g |= 'not' H by A5, Th14;
hence E,f |= Ex x,H by A1, A4, Th16; :: thesis: verum