Theorem cbvralvw2

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

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

Proof

Step	Hyp	Ref	Expression
1		cbvralvw2.1	$$⊢x=y\to A=B$$
2		cbvralvw2.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	imbi12d	$$⊢x=y\to \left(\left(x\in A\to \phi \right)\leftrightarrow \left(y\in B\to \psi \right)\right)$$
7	6	cbvalvw	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall y\left(y\in B\to \psi \right)$$
8		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
9		df-ral	$$⊢\forall y\in B\psi \leftrightarrow \forall y\left(y\in B\to \psi \right)$$
10	7 8 9	3bitr4i	$$⊢\forall x\in A\phi \leftrightarrow \forall y\in B\psi$$