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