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