Theorem cbvriota

Description: Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvriotaw when possible. (Contributed by NM, 18-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvriota.1	⊢ Ⅎ 𝑦 𝜑
	cbvriota.2	⊢ Ⅎ 𝑥 𝜓
	cbvriota.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvriota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑦 ∈ 𝐴 𝜓 )

Proof

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