Theorem cbvrabcsf

Description: A more general version of cbvrab with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		cbvralcsf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		cbvralcsf.3	$$⊢Ⅎy\phi$$
4		cbvralcsf.4	$$⊢Ⅎx\psi$$
5		cbvralcsf.5	$$⊢x=y\to A=B$$
6		cbvralcsf.6	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
7		nfv	$$⊢Ⅎz\left(x\in A\wedge \phi \right)$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌A$$
9	8	nfcri	$$⊢Ⅎxz\in ⦋z/x⦌A$$
10		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
11	9 10	nfan	$$⊢Ⅎx\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)$$
12		id	$$⊢x=z\to x=z$$
13		csbeq1a	$$⊢x=z\to A=⦋z/x⦌A$$
14	12 13	eleq12d	$$⊢x=z\to \left(x\in A\leftrightarrow z\in ⦋z/x⦌A\right)$$
15		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
16	14 15	anbi12d	$$⊢x=z\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\right)$$
17	7 11 16	cbvab	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{z|\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\right\}$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
19	18 1	nfcsb	$$⊢\underset{\_}{Ⅎ}y⦋z/x⦌A$$
20	19	nfcri	$$⊢Ⅎyz\in ⦋z/x⦌A$$
21	3	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
22	20 21	nfan	$$⊢Ⅎy\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)$$
23		nfv	$$⊢Ⅎz\left(y\in B\wedge \psi \right)$$
24		id	$$⊢z=y\to z=y$$
25		csbeq1	$$⊢z=y\to ⦋z/x⦌A=⦋y/x⦌A$$
26		df-csb	$$⊢⦋y/x⦌A=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
27	2	nfcri	$$⊢Ⅎxv\in B$$
28	5	eleq2d	$$⊢x=y\to \left(v\in A\leftrightarrow v\in B\right)$$
29	27 28	sbie	$$⊢\left[y/x\right]v\in A\leftrightarrow v\in B$$
30		sbsbc	$$⊢\left[y/x\right]v\in A\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A$$
31	29 30	bitr3i	$$⊢v\in B\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A$$
32	31	abbi2i	$$⊢B=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
33	26 32	eqtr4i	$$⊢⦋y/x⦌A=B$$
34	25 33	eqtrdi	$$⊢z=y\to ⦋z/x⦌A=B$$
35	24 34	eleq12d	$$⊢z=y\to \left(z\in ⦋z/x⦌A\leftrightarrow y\in B\right)$$
36		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
37	4 6	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
38	36 37	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
39	35 38	anbi12d	$$⊢z=y\to \left(\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\leftrightarrow \left(y\in B\wedge \psi \right)\right)$$
40	22 23 39	cbvab	$$⊢\left\{z|\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\right\}=\left\{y|\left(y\in B\wedge \psi \right)\right\}$$
41	17 40	eqtri	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\left(y\in B\wedge \psi \right)\right\}$$
42		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
43		df-rab	$$⊢\left\{y\in B|\psi \right\}=\left\{y|\left(y\in B\wedge \psi \right)\right\}$$
44	41 42 43	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}=\left\{y\in B|\psi \right\}$$