let H be ZF-formula; for x being Variable
for M being non empty set holds M |= H => (Ex (x,H))
let x be Variable; for M being non empty set holds M |= H => (Ex (x,H))
let M be non empty set ; M |= H => (Ex (x,H))
let v be Function of VAR,M; ZF_MODEL:def 5 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; verum