let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st H is being_membership holds
( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
let M be non empty set ; :: thesis: for v being Function of VAR,M st H is being_membership holds
( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
let v be Function of VAR,M; :: thesis: ( H is being_membership implies ( M,v |= H iff v . (Var1 H) in v . (Var2 H) ) )
assume H is being_membership ; :: thesis: ( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
then H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
hence ( M,v |= H iff v . (Var1 H) in v . (Var2 H) ) by ZF_MODEL:13; :: thesis: verum