theorem :: ZF_LANG1:90

for H being ZF-formula
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 ) )