let H be ZF-formula; :: thesis: 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 )
let x, y be Variable; :: thesis: ( H is conditional implies ( the_antecedent_of (H / x,y) = (the_antecedent_of H) / x,y & the_consequent_of (H / x,y) = (the_consequent_of H) / x,y ) )
assume H is conditional ; :: thesis: ( the_antecedent_of (H / x,y) = (the_antecedent_of H) / x,y & the_consequent_of (H / x,y) = (the_consequent_of H) / x,y )
then ( H / x,y is conditional & H = (the_antecedent_of H) => (the_consequent_of H) ) by Th189, ZF_LANG:65;
then ( H / x,y = (the_antecedent_of (H / x,y)) => (the_consequent_of (H / x,y)) & H / x,y = ((the_antecedent_of H) / x,y) => ((the_consequent_of H) / x,y) ) by Th176, ZF_LANG:65;
hence ( the_antecedent_of (H / x,y) = (the_antecedent_of H) / x,y & the_consequent_of (H / x,y) = (the_consequent_of H) / x,y ) by ZF_LANG:49; :: thesis: verum