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