cbvrab

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrabw when possible. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvrab.1	⊢ Ⅎ 𝑥 𝐴
	cbvrab.2	⊢ Ⅎ 𝑦 𝐴
	cbvrab.3	⊢ Ⅎ 𝑦 𝜑
	cbvrab.4	⊢ Ⅎ 𝑥 𝜓
	cbvrab.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvrab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvrab.1	⊢ Ⅎ 𝑥 𝐴
2		cbvrab.2	⊢ Ⅎ 𝑦 𝐴
3		cbvrab.3	⊢ Ⅎ 𝑦 𝜑
4		cbvrab.4	⊢ Ⅎ 𝑥 𝜓
5		cbvrab.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
7	1	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
8		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
9	7 8	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
10		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
11		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
12	10 11	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
13	6 9 12	cbvab	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
14	2	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
15	3	nfsb	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
16	14 15	nfan	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
17		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐴 ∧ 𝜓 )
18		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
19		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
20	4 5	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
21	19 20	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
22	18 21	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
23	16 17 22	cbvab	⊢ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) }
24	13 23	eqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) }
25		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
26		df-rab	⊢ { 𝑦 ∈ 𝐴 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) }
27	24 25 26	3eqtr4i	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 }

Metamath Proof Explorer

Theorem cbvrab

Proof