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)) implies not E,f |= All x,('not' H) ) & ( not E,f |= All x,('not' H) implies E,f |= 'not' (All x,('not' H)) ) & ( E,f |= All x,('not' H) implies for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= 'not' H ) & ( ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= 'not' H ) implies E,f |= All x,('not' H) ) & ( E,f |= 'not' H implies not E,f |= H ) & ( not E,f |= H implies E,f |= 'not' H ) )
by Th14, Th16;
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 ) & not
E,
g |= 'not' H )
by A1;
E,
g |= H
by A2, 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 A3:
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H )
; :: thesis: E,f |= Ex x,H
not E,g |= 'not' H
by A3, Th14;
hence
E,f |= Ex x,H
by A1, A3; :: thesis: verum