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

Metamath Proof Explorer

Theorem csbiota

Description: Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017) (Revised by NM, 23-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑧 = 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) )
2 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3 2 iotabidv ⊢ ( 𝑧 = 𝐴 → ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
4 1 3 eqeq12d ⊢ ( 𝑧 = 𝐴 → ( ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) ) )
5 vex ⊢ 𝑧 ∈ V
6 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
7 6 nfiotaw ⊢ Ⅎ 𝑥 ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
8 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
9 8 iotabidv ⊢ ( 𝑥 = 𝑧 → ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) )
10 5 7 9 csbief ⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
11 4 10 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
12 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ∅ )
13 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
14 13 con3i ⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝜑 )
15 14 nexdv ⊢ ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
16 euex ⊢ ( ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
17 16 con3i ⊢ ( ¬ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ¬ ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
18 iotanul ⊢ ( ¬ ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) = ∅ )
19 15 17 18 3syl ⊢ ( ¬ 𝐴 ∈ V → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) = ∅ )
20 12 19 eqtr4d ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
21 11 20 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )