let H be 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 ) )
let x, y be 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 ) )
let E be 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 ) )
let f be Function of VAR,E; ( 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 ) )
thus
( E,f |= Ex (x,y,H) implies 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 ) )
( 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 ) implies E,f |= Ex (x,y,H) )proof
assume
E,
f |= Ex (
x,
y,
H)
;
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 )
then consider g being
Function of
VAR,
E such that A1:
for
z being
Variable st
g . z <> f . z holds
x = z
and A2:
E,
g |= Ex (
y,
H)
by Th20;
consider h being
Function of
VAR,
E such that A3:
for
z being
Variable st
h . z <> g . z holds
y = z
and A4:
E,
h |= H
by A2, Th20;
take
h
;
( ( for z being Variable holds
( not h . z <> f . z or x = z or y = z ) ) & E,h |= H )
thus
for
z being
Variable holds
( not
h . z <> f . z or
x = z or
y = z )
E,h |= Hproof
let z be
Variable;
( not h . z <> f . z or x = z or y = z )
assume that A5:
h . z <> f . z
and A6:
x <> z
and A7:
y <> z
;
contradiction
g . z = f . z
by A1, A6;
hence
contradiction
by A3, A5, A7;
verum
end;
thus
E,
h |= H
by A4;
verum
end;
given g being Function of VAR,E such that A8:
for z being Variable holds
( not g . z <> f . z or x = z or y = z )
and
A9:
E,g |= H
; E,f |= Ex (x,y,H)
set h = f +* (x,(g . x));
then A13:
E,f +* (x,(g . x)) |= Ex (y,H)
by A9, Th20;
for z being Variable st (f +* (x,(g . x))) . z <> f . z holds
x = z
by FUNCT_7:32;
hence
E,f |= Ex (x,y,H)
by A13, Th20; verum