let H2, H1 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 A1: ( not x in Free H2 & ( 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
( ( for m being Element of M holds M,v / x,m |= H1 => H2 ) & M |= (All x,(H1 => H2)) => ((Ex x,H1) => H2) ) by A1, Th142;
then ( M,v |= (All x,(H1 => H2)) => ((Ex x,H1) => H2) & M,v |= All x,(H1 => H2) ) by Th80, ZF_MODEL:def 5;
hence M,v |= (Ex x,H1) => H2 by ZF_MODEL:18; :: thesis: verum