let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set holds M |= H => (Ex x,H)
let x be Variable; :: thesis: for M being non empty set holds M |= H => (Ex x,H)
let M be non empty set ; :: thesis: M |= H => (Ex x,H)
let v be Function of VAR ,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= H => (Ex x,H)
( M,v / x,(v . x) |= H implies M,v |= Ex x,H ) by Th82;
then ( M,v |= H implies M,v |= Ex x,H ) by FUNCT_7:37;
hence M,v |= H => (Ex x,H) by ZF_MODEL:18; :: thesis: verum