theorem :: ZF_LANG1:173

for H being ZF-formula
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 ) )