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	⊢ Ⅎ 𝑦 𝐴
	cbvrabcsfw.2	⊢ Ⅎ 𝑥 𝐵
	cbvrabcsfw.3	⊢ Ⅎ 𝑦 𝜑
	cbvrabcsfw.4	⊢ Ⅎ 𝑥 𝜓
	cbvrabcsfw.5	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	cbvrabcsfw.6	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvrabcsfw	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvrabcsfw.1	⊢ Ⅎ 𝑦 𝐴
2		cbvrabcsfw.2	⊢ Ⅎ 𝑥 𝐵
3		cbvrabcsfw.3	⊢ Ⅎ 𝑦 𝜑
4		cbvrabcsfw.4	⊢ Ⅎ 𝑥 𝜓
5		cbvrabcsfw.5	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
6		cbvrabcsfw.6	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
7		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
9	8	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
10		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
11	9 10	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
12		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
13		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
14	12 13	eleq12d	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
15		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
16	14 15	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
17	7 11 16	cbvabw	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
18		nfcv	⊢ Ⅎ 𝑦 𝑧
19	18 1	nfcsbw	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
20	19	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
21	3	nfsbv	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
22	20 21	nfan	⊢ Ⅎ 𝑦 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
23		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 ∧ 𝜓 )
24		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
25		csbeq1	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
26		vex	⊢ 𝑦 ∈ V
27	26 2 5	csbief	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵
28	25 27	eqtrdi	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐵 )
29	24 28	eleq12d	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
30	4 6	sbhypf	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
31	29 30	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) )
32	22 23 31	cbvabw	⊢ { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
33	17 32	eqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
34		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
35		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
36	33 34 35	3eqtr4i	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 }