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