let H be ZF-formula; for x, y being Variable st H is existential 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; ( H is existential 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 existential
; ( 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 existential
by Th177;
then A2:
H / (x,y) = Ex ((bound_in (H / (x,y))),(the_scope_of (H / (x,y))))
by ZF_LANG:45;
A3:
H = Ex ((bound_in H),(the_scope_of H))
by A1, ZF_LANG:45;
then A4:
( bound_in H <> x implies H / (x,y) = Ex ((bound_in H),((the_scope_of H) / (x,y))) )
by Th164;
( bound_in H = x implies H / (x,y) = Ex (y,((the_scope_of H) / (x,y))) )
by A3, Th165;
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:34; verum