Theorem cbvrab

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrabw when possible. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrab.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		cbvrab.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		cbvrab.3	$$⊢Ⅎy\phi$$
4		cbvrab.4	$$⊢Ⅎx\psi$$
5		cbvrab.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6		nfv	$$⊢Ⅎz\left(x\in A\wedge \phi \right)$$
7	1	nfcri	$$⊢Ⅎxz\in A$$
8		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
9	7 8	nfan	$$⊢Ⅎx\left(z\in A\wedge \left[z/x\right]\phi \right)$$
10		eleq1w	$$⊢x=z\to \left(x\in A\leftrightarrow z\in A\right)$$
11		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
12	10 11	anbi12d	$$⊢x=z\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(z\in A\wedge \left[z/x\right]\phi \right)\right)$$
13	6 9 12	cbvab	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{z|\left(z\in A\wedge \left[z/x\right]\phi \right)\right\}$$
14	2	nfcri	$$⊢Ⅎyz\in A$$
15	3	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
16	14 15	nfan	$$⊢Ⅎy\left(z\in A\wedge \left[z/x\right]\phi \right)$$
17		nfv	$$⊢Ⅎz\left(y\in A\wedge \psi \right)$$
18		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
19		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
20	4 5	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
21	19 20	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
22	18 21	anbi12d	$$⊢z=y\to \left(\left(z\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \left(y\in A\wedge \psi \right)\right)$$
23	16 17 22	cbvab	$$⊢\left\{z|\left(z\in A\wedge \left[z/x\right]\phi \right)\right\}=\left\{y|\left(y\in A\wedge \psi \right)\right\}$$
24	13 23	eqtri	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\left(y\in A\wedge \psi \right)\right\}$$
25		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
26		df-rab	$$⊢\left\{y\in A|\psi \right\}=\left\{y|\left(y\in A\wedge \psi \right)\right\}$$
27	24 25 26	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}=\left\{y\in A|\psi \right\}$$