let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set holds
( M |= Ex x,H iff for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H )
let x be Variable; :: thesis: for M being non empty set holds
( M |= Ex x,H iff for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H )
let M be non empty set ; :: thesis: ( M |= Ex x,H iff for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H )
thus
( M |= Ex x,H implies for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H )
:: thesis: ( ( for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H ) implies M |= Ex x,H )proof
assume A1:
for
v being
Function of
VAR ,
M holds
M,
v |= Ex x,
H
;
:: according to ZF_MODEL:def 5 :: thesis: for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H
let v be
Function of
VAR ,
M;
:: thesis: ex m being Element of M st M,v / x,m |= H
M,
v |= Ex x,
H
by A1;
hence
ex
m being
Element of
M st
M,
v / x,
m |= H
by Th82;
:: thesis: verum
end;
assume A2:
for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H
; :: thesis: M |= Ex x,H
let v be Function of VAR ,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= Ex x,H
ex m being Element of M st M,v / x,m |= H
by A2;
hence
M,v |= Ex x,H
by Th82; :: thesis: verum