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 | E. w <. y , w >. e. B } = { y | [. A / x ]. E. w <. y , w >. e. B }
2 sbcex2 
 |-  ( [. A / x ]. E. w <. y , w >. e. B <-> E. w [. A / x ]. <. y , w >. e. B )
3 sbcel2 
 |-  ( [. A / x ]. <. y , w >. e. B <-> <. y , w >. e. [_ A / x ]_ B )
4 3 exbii 
 |-  ( E. w [. A / x ]. <. y , w >. e. B <-> E. w <. y , w >. e. [_ A / x ]_ B )
5 2 4 bitri 
 |-  ( [. A / x ]. E. w <. y , w >. e. B <-> E. w <. y , w >. e. [_ A / x ]_ B )
6 5 abbii 
 |-  { y | [. A / x ]. E. w <. y , w >. e. B } = { y | E. w <. y , w >. e. [_ A / x ]_ B }
7 1 6 eqtri 
 |-  [_ A / x ]_ { y | E. w <. y , w >. e. B } = { y | E. w <. y , w >. e. [_ A / x ]_ B }
8 dfdm3 
 |-  dom B = { y | E. w <. y , w >. e. B }
9 8 csbeq2i 
 |-  [_ A / x ]_ dom B = [_ A / x ]_ { y | E. w <. y , w >. e. B }
10 dfdm3 
 |-  dom [_ A / x ]_ B = { y | E. w <. y , w >. e. [_ A / x ]_ B }
11 7 9 10 3eqtr4i 
 |-  [_ A / x ]_ dom B = dom [_ A / x ]_ B