let H be ZF-formula; :: thesis: for x, y being Variable st H is universal holds
( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
let x, y be Variable; :: thesis: ( H is universal implies ( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) ) )
assume A1: H is universal ; :: thesis: ( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
then H / (x,y) is universal by Th170;
then A2: H / (x,y) = All ((bound_in (H / (x,y))),(the_scope_of (H / (x,y)))) by ZF_LANG:44;
A3: H = All ((bound_in H),(the_scope_of H)) by A1, ZF_LANG:44;
then A4: ( bound_in H <> x implies H / (x,y) = All ((bound_in H),((the_scope_of H) / (x,y))) ) by Th159;
( bound_in H = x implies H / (x,y) = All (y,((the_scope_of H) / (x,y))) ) by A3, Th160;
hence ( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) ) by A2, A4, ZF_LANG:3; :: thesis: verum