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

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	⊢ Ⅎ 𝑦 𝐴
2		cbvralcsf.2	⊢ Ⅎ 𝑥 𝐵
3		cbvralcsf.3	⊢ Ⅎ 𝑦 𝜑
4		cbvralcsf.4	⊢ Ⅎ 𝑥 𝜓
5		cbvralcsf.5	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
6		cbvralcsf.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	cbvab	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
18		nfcv	⊢ Ⅎ 𝑦 𝑧
19	18 1	nfcsb	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
20	19	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
21	3	nfsb	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
22	20 21	nfan	⊢ Ⅎ 𝑦 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
23		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 ∧ 𝜓 )
24		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
25		csbeq1	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
26		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
27	2	nfcri	⊢ Ⅎ 𝑥 𝑣 ∈ 𝐵
28	5	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 ) )
29	27 28	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 )
30		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
31	29 30	bitr3i	⊢ ( 𝑣 ∈ 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
32	31	eqabi	⊢ 𝐵 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
33	26 32	eqtr4i	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵
34	25 33	eqtrdi	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐵 )
35	24 34	eleq12d	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
36		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
37	4 6	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
38	36 37	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
39	35 38	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) )
40	22 23 39	cbvab	⊢ { 𝑧 ∣ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
41	17 40	eqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
42		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
43		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) }
44	41 42 43	3eqtr4i	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ 𝜓 }

Metamath Proof Explorer

Theorem cbvrabcsf

Proof