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