Description: Changing a bound variable (existential quantification case) in a weak
axiomatization, assuming that all variables denote (which is valid in
inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023)(Proof modification is discouraged.)