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

Metamath Proof Explorer

Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

Ref Expression
Assertion csbab ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 }

Proof

Step Hyp Ref Expression
1 df-clab ⊢ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
2 sbsbc ⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
3 1 2 bitri ⊢ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
4 sbccom ⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
5 df-clab ⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
6 sbsbc ⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 )
7 5 6 bitri ⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
8 7 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
9 4 8 bitr4i ⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } )
10 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } )
11 3 9 10 3bitrri ⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } )
12 11 eqriv ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 }