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 GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	cbvrabcsfw.1	|- F/_ y A
	cbvrabcsfw.2	|- F/_ x B
	cbvrabcsfw.3	|- F/ y ph
	cbvrabcsfw.4	|- F/ x ps
	cbvrabcsfw.5	|- ( x = y -> A = B )
	cbvrabcsfw.6	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvrabcsfw	|- { x e. A | ph } = { y e. B | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvrabcsfw.1	|- F/_ y A
2		cbvrabcsfw.2	|- F/_ x B
3		cbvrabcsfw.3	|- F/ y ph
4		cbvrabcsfw.4	|- F/ x ps
5		cbvrabcsfw.5	|- ( x = y -> A = B )
6		cbvrabcsfw.6	|- ( x = y -> ( ph <-> ps ) )
7		nfv	|- F/ z ( x e. A /\ ph )
8		nfcsb1v	|- F/_ x [_ z / x ]_ A
9	8	nfcri	|- F/ x z e. [_ z / x ]_ A
10		nfs1v	|- F/ x [ z / x ] ph
11	9 10	nfan	|- F/ x ( z e. [_ z / x ]_ A /\ [ z / x ] ph )
12		id	|- ( x = z -> x = z )
13		csbeq1a	|- ( x = z -> A = [_ z / x ]_ A )
14	12 13	eleq12d	|- ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) )
15		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
16	14 15	anbi12d	|- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) ) )
17	7 11 16	cbvabw	|- { x | ( x e. A /\ ph ) } = { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) }
18		nfcv	|- F/_ y z
19	18 1	nfcsbw	|- F/_ y [_ z / x ]_ A
20	19	nfcri	|- F/ y z e. [_ z / x ]_ A
21	3	nfsbv	|- F/ y [ z / x ] ph
22	20 21	nfan	|- F/ y ( z e. [_ z / x ]_ A /\ [ z / x ] ph )
23		nfv	|- F/ z ( y e. B /\ ps )
24		id	|- ( z = y -> z = y )
25		csbeq1	|- ( z = y -> [_ z / x ]_ A = [_ y / x ]_ A )
26		vex	|- y e. _V
27	26 2 5	csbief	|- [_ y / x ]_ A = B
28	25 27	eqtrdi	|- ( z = y -> [_ z / x ]_ A = B )
29	24 28	eleq12d	|- ( z = y -> ( z e. [_ z / x ]_ A <-> y e. B ) )
30	4 6	sbhypf	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
31	29 30	anbi12d	|- ( z = y -> ( ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) <-> ( y e. B /\ ps ) ) )
32	22 23 31	cbvabw	|- { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) } = { y | ( y e. B /\ ps ) }
33	17 32	eqtri	|- { x | ( x e. A /\ ph ) } = { y | ( y e. B /\ ps ) }
34		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
35		df-rab	|- { y e. B | ps } = { y | ( y e. B /\ ps ) }
36	33 34 35	3eqtr4i	|- { x e. A | ph } = { y e. B | ps }