Theorem cbvrexvw2

Description: Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvrexvw2.1	$$⊢x=y\to A=B$$
	cbvrexvw2.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvrexvw2	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvrexvw2.1	$$⊢x=y\to A=B$$
2		cbvrexvw2.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
4	1	eleq2d	$$⊢x=y\to \left(y\in A\leftrightarrow y\in B\right)$$
5	3 4	bitrd	$$⊢x=y\to \left(x\in A\leftrightarrow y\in B\right)$$
6	5 2	anbi12d	$$⊢x=y\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(y\in B\wedge \psi \right)\right)$$
7	6	cbvexvw	$$⊢\exists x\left(x\in A\wedge \phi \right)\leftrightarrow \exists y\left(y\in B\wedge \psi \right)$$
8		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
9		df-rex	$$⊢\exists y\in B\psi \leftrightarrow \exists y\left(y\in B\wedge \psi \right)$$
10	7 8 9	3bitr4i	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in B\psi$$