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