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

Metamath Proof Explorer

Theorem csbsng

Description: Distribute proper substitution through the singleton of a class. csbsng is derived from the virtual deduction proof csbsngVD . (Contributed by Alan Sare, 10-Nov-2012)

Ref Expression
Assertion csbsng ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )

Proof

Step Hyp Ref Expression
1 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 }
2 sbceq2g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 ↔ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
3 2 abbidv ⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
4 1 3 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
5 df-sn ⊢ { 𝐵 } = { 𝑦 ∣ 𝑦 = 𝐵 }
6 5 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 }
7 df-sn ⊢ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
8 4 6 7 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )