Theorem cbvreuvw2

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

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

Proof

Step	Hyp	Ref	Expression
1		cbvreuvw2.1	$$⊢x=y\to A=B$$
2		cbvreuvw2.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	cbveuvw	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \exists !y\left(y\in B\wedge \psi \right)$$
8		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
9		df-reu	$$⊢\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$$