Theorem cbvrabcsfw

Description: Version of cbvrabcsf with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrabcsfw.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		cbvrabcsfw.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		cbvrabcsfw.3	$$⊢Ⅎy\phi$$
4		cbvrabcsfw.4	$$⊢Ⅎx\psi$$
5		cbvrabcsfw.5	$$⊢x=y\to A=B$$
6		cbvrabcsfw.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	cbvabw	$$⊢\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	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋z/x⦌A$$
20	19	nfcri	$$⊢Ⅎyz\in ⦋z/x⦌A$$
21	3	nfsbv	$$⊢Ⅎ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		vex	$$⊢y\in \mathrm{V}$$
27	26 2 5	csbief	$$⊢⦋y/x⦌A=B$$
28	25 27	syl6eq	$$⊢z=y\to ⦋z/x⦌A=B$$
29	24 28	eleq12d	$$⊢z=y\to \left(z\in ⦋z/x⦌A\leftrightarrow y\in B\right)$$
30	4 6	sbhypf	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
31	29 30	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)$$
32	22 23 31	cbvabw	$$⊢\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\}$$
33	17 32	eqtri	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\left(y\in B\wedge \psi \right)\right\}$$
34		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
35		df-rab	$$⊢\left\{y\in B|\psi \right\}=\left\{y|\left(y\in B\wedge \psi \right)\right\}$$
36	33 34 35	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}=\left\{y\in B|\psi \right\}$$