Theorem cbvrexdva

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 9-Mar-2025)

	Ref	Expression
Hypothesis	cbvraldva.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbvrexdva	|- ( ph -> ( E. x e. A ps <-> E. y e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbvraldva.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2	1	notbid	|- ( ( ph /\ x = y ) -> ( -. ps <-> -. ch ) )
3	2	cbvraldva	|- ( ph -> ( A. x e. A -. ps <-> A. y e. A -. ch ) )
4		ralnex	|- ( A. x e. A -. ps <-> -. E. x e. A ps )
5		ralnex	|- ( A. y e. A -. ch <-> -. E. y e. A ch )
6	3 4 5	3bitr3g	|- ( ph -> ( -. E. x e. A ps <-> -. E. y e. A ch ) )
7	6	con4bid	|- ( ph -> ( E. x e. A ps <-> E. y e. A ch ) )