let H1, H2 be ZF-formula; :: thesis: for x being Variable
for M being non empty set st not x in Free H2 holds
M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
let x be Variable; :: thesis: for M being non empty set st not x in Free H2 holds
M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
let M be non empty set ; :: thesis: ( not x in Free H2 implies M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) )
assume A1: not x in Free H2 ; :: thesis: M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)

now :: thesis: ( M,v |= All (x,(H1 => H2)) implies M,v |= (Ex (x,H1)) => H2 )

assume A2: M,v |= All (x,(H1 => H2)) ; :: thesis: M,v |= (Ex (x,H1)) => H2

now :: thesis: ( M,v |= Ex (x,H1) implies M,v |= H2 )

assume M,v |= Ex (x,H1) ; :: thesis: M,v |= H2
then consider m being Element of M such that
A3: M,v / (x,m) |= H1 by Th73;
M,v / (x,m) |= H1 => H2 by A2, Th71;
then M,v / (x,m) |= H2 by A3, ZF_MODEL:18;
then M,v / (x,m) |= All (x,H2) by A1, ZFMODEL1:10;
then M,v |= All (x,H2) by Th72;
then M,v / (x,(v . x)) |= H2 by Th71;
hence M,v |= H2 by FUNCT_7:35; :: thesis: verum

end;

hence M,v |= (Ex (x,H1)) => H2 by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) by ZF_MODEL:18; :: thesis: verum