let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st H is conditional holds
( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
let M be non empty set ; :: thesis: for v being Function of VAR,M st H is conditional holds
( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
let v be Function of VAR,M; :: thesis: ( H is conditional implies ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) ) )
assume H is conditional ; :: thesis: ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
then H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
hence ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) ) by ZF_MODEL:18; :: thesis: verum