Theorem cbvriotaw

Description: Change bound variable in a restricted description binder. Version of cbvriota with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Mar-2013) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

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