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:62;
hence ( M,v |= H iff for m being Element of M holds M,v / (bound_in H),m |= the_scope_of H ) by Th80; :: thesis: verum