Theorem cbvrmovw2

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

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

Proof

Step	Hyp	Ref	Expression
1		cbvrmovw2.1	$$⊢x=y\to A=B$$
2		cbvrmovw2.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	cbvmovw	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\leftrightarrow {\exists }^{*}y\left(y\in B\wedge \psi \right)$$
8		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
9		df-rmo	$$⊢{\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$$