Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 19-Jul-2025)

	Ref	Expression
Hypotheses	cbvrabw.1	$$⊢\underset{\_}{Ⅎ}xA$$
	cbvrabw.2	$$⊢\underset{\_}{Ⅎ}yA$$
	cbvrabw.3	$$⊢Ⅎy\phi$$
	cbvrabw.4	$$⊢Ⅎx\psi$$
	cbvrabw.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvrabw	$$⊢\left\{x\in A|\phi \right\}=\left\{y\in A|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvrabw.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		cbvrabw.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		cbvrabw.3	$$⊢Ⅎy\phi$$
4		cbvrabw.4	$$⊢Ⅎx\psi$$
5		cbvrabw.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6	2	nfcri	$$⊢Ⅎyx\in A$$
7	6 3	nfan	$$⊢Ⅎy\left(x\in A\wedge \phi \right)$$
8	1	nfcri	$$⊢Ⅎxy\in A$$
9	8 4	nfan	$$⊢Ⅎx\left(y\in A\wedge \psi \right)$$
10		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
11	10 5	anbi12d	$$⊢x=y\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(y\in A\wedge \psi \right)\right)$$
12	7 9 11	cbvabw	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\left(y\in A\wedge \psi \right)\right\}$$
13		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
14		df-rab	$$⊢\left\{y\in A|\psi \right\}=\left\{y|\left(y\in A\wedge \psi \right)\right\}$$
15	12 13 14	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}=\left\{y\in A|\psi \right\}$$