let H1, H2 be ZF-formula; :: thesis: for x being Variable
for M being non empty set st not x in Free H2 & M |= H1 => H2 holds
M |= (Ex (x,H1)) => H2
let x be Variable; :: thesis: for M being non empty set st not x in Free H2 & M |= H1 => H2 holds
M |= (Ex (x,H1)) => H2
let M be non empty set ; :: thesis: ( not x in Free H2 & M |= H1 => H2 implies M |= (Ex (x,H1)) => H2 )
assume that
A1: not x in Free H2 and
A2: for v being Function of VAR,M holds M,v |= H1 => H2 ; :: according to ZF_MODEL:def 5 :: thesis: M |= (Ex (x,H1)) => H2
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= (Ex (x,H1)) => H2
M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) by A1, Th130;
then A3: M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) ;
for m being Element of M holds M,v / (x,m) |= H1 => H2 by A2;
then M,v |= All (x,(H1 => H2)) by Th71;
hence M,v |= (Ex (x,H1)) => H2 by A3, ZF_MODEL:18; :: thesis: verum