theorem :: ZF_LANG1:179

for H being ZF-formula
for x, y being Variable st H is conditional holds
( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) )