let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st H is universal holds
( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
let M be non empty set ; :: thesis: for v being Function of VAR,M st H is universal holds
( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
let v be Function of VAR,M; :: thesis: ( H is universal implies ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H ) )
assume H is universal ; :: thesis: ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
then H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
hence ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H ) by Th71; :: thesis: verum