let H be ZF-formula; for x being Variable
for M being non empty set st M |= H holds
M |= Ex (x,H)
let x be Variable; for M being non empty set st M |= H holds
M |= Ex (x,H)
let M be non empty set ; ( M |= H implies M |= Ex (x,H) )
assume A1:
M |= H
; M |= Ex (x,H)
let v be Function of VAR,M; ZF_MODEL:def 5 M,v |= Ex (x,H)
M,v / (x,(v . x)) |= H
by A1;
hence
M,v |= Ex (x,H)
by Th73; verum