let H be ZF-formula; :: thesis: for x, y being Variable st H is conjunctive holds
( the_left_argument_of (H / x,y) = (the_left_argument_of H) / x,y & the_right_argument_of (H / x,y) = (the_right_argument_of H) / x,y )
let x, y be Variable; :: thesis: ( H is conjunctive implies ( the_left_argument_of (H / x,y) = (the_left_argument_of H) / x,y & the_right_argument_of (H / x,y) = (the_right_argument_of H) / x,y ) )
assume A1: H is conjunctive ; :: thesis: ( the_left_argument_of (H / x,y) = (the_left_argument_of H) / x,y & the_right_argument_of (H / x,y) = (the_right_argument_of H) / x,y )
then H / x,y is conjunctive by Th183;
then A2: H / x,y = (the_left_argument_of (H / x,y)) '&' (the_right_argument_of (H / x,y)) by ZF_LANG:58;
H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1, ZF_LANG:58;
hence ( the_left_argument_of (H / x,y) = (the_left_argument_of H) / x,y & the_right_argument_of (H / x,y) = (the_right_argument_of H) / x,y ) by A2, Th172; :: thesis: verum