This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑦 ∈ 𝐴 𝜓 )