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

Metamath Proof Explorer

Theorem csbriota

Description: Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013) (Revised by NM, 2-Sep-2018)

Ref Expression
Assertion csbriota ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑧 = 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) )
2 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3 2 riotabidv ⊢ ( 𝑧 = 𝐴 → ( ℩ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
4 1 3 eqeq12d ⊢ ( 𝑧 = 𝐴 → ( ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) ) )
5 vex ⊢ 𝑧 ∈ V
6 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
7 nfcv ⊢ Ⅎ 𝑥 𝐵
8 6 7 nfriota ⊢ Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
9 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
10 9 riotabidv ⊢ ( 𝑥 = 𝑧 → ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ) )
11 5 8 10 csbief ⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
12 4 11 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
13 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ∅ )
14 df-riota ⊢ ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
15 euex ⊢ ( ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
16 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
17 16 adantl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 ∈ V )
18 17 exlimiv ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 ∈ V )
19 15 18 syl ⊢ ( ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 ∈ V )
20 iotanul ⊢ ( ¬ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) = ∅ )
21 19 20 nsyl5 ⊢ ( ¬ 𝐴 ∈ V → ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) = ∅ )
22 14 21 eqtr2id ⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
23 13 22 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
24 12 23 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 ∈ 𝐵 𝜑 ) = ( ℩ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )