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 Th73;
then ( M,v |= H implies M,v |= Ex (x,H) ) by FUNCT_7:35;
hence M,v |= H => (Ex (x,H)) by ZF_MODEL:18; :: thesis: verum