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 ⊢ ⦋ A / x⦌ dom ⁡ B = dom ⁡ ⦋ A / x⦌ B

Proof

Step Hyp Ref Expression
1 csbab ⊢ ⦋ A / x⦌ y | ∃ w y w ∈ B = y | [˙A / x]˙ ∃ w y w ∈ B
2 sbcex2 ⊢ [˙A / x]˙ ∃ w y w ∈ B ↔ ∃ w [˙A / x]˙ y w ∈ B
3 sbcel2 ⊢ [˙A / x]˙ y w ∈ B ↔ y w ∈ ⦋ A / x⦌ B
4 3 exbii ⊢ ∃ w [˙A / x]˙ y w ∈ B ↔ ∃ w y w ∈ ⦋ A / x⦌ B
5 2 4 bitri ⊢ [˙A / x]˙ ∃ w y w ∈ B ↔ ∃ w y w ∈ ⦋ A / x⦌ B
6 5 abbii ⊢ y | [˙A / x]˙ ∃ w y w ∈ B = y | ∃ w y w ∈ ⦋ A / x⦌ B
7 1 6 eqtri ⊢ ⦋ A / x⦌ y | ∃ w y w ∈ B = y | ∃ w y w ∈ ⦋ A / x⦌ B
8 dfdm3 ⊢ dom ⁡ B = y | ∃ w y w ∈ B
9 8 csbeq2i ⊢ ⦋ A / x⦌ dom ⁡ B = ⦋ A / x⦌ y | ∃ w y w ∈ B
10 dfdm3 ⊢ dom ⁡ ⦋ A / x⦌ B = y | ∃ w y w ∈ ⦋ A / x⦌ B
11 7 9 10 3eqtr4i ⊢ ⦋ A / x⦌ dom ⁡ B = dom ⁡ ⦋ A / x⦌ B