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

Metamath Proof Explorer

Theorem csbdm

Description: Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017) (Revised by NM, 24-Aug-2018)

Ref Expression
Assertion csbdm ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step Hyp Ref Expression
1 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
2 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 )
3 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4 3 exbii ⊢ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
5 2 4 bitri ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
6 5 abbii ⊢ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
7 1 6 eqtri ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
8 dfdm3 ⊢ dom 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
9 8 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
10 dfdm3 ⊢ dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
11 7 9 10 3eqtr4i ⊢ ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵