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⦌\mathrm{dom}B=\mathrm{dom}⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		csbab	$$⊢⦋A/x⦌\left\{y|\exists w⟨y,w⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨y,w⟩\in B\right\}$$
2		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨y,w⟩\in B\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨y,w⟩\in B$$
3		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨y,w⟩\in B\leftrightarrow ⟨y,w⟩\in ⦋A/x⦌B$$
4	3	exbii	$$⊢\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨y,w⟩\in B\leftrightarrow \exists w⟨y,w⟩\in ⦋A/x⦌B$$
5	2 4	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨y,w⟩\in B\leftrightarrow \exists w⟨y,w⟩\in ⦋A/x⦌B$$
6	5	abbii	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨y,w⟩\in B\right\}=\left\{y|\exists w⟨y,w⟩\in ⦋A/x⦌B\right\}$$
7	1 6	eqtri	$$⊢⦋A/x⦌\left\{y|\exists w⟨y,w⟩\in B\right\}=\left\{y|\exists w⟨y,w⟩\in ⦋A/x⦌B\right\}$$
8		dfdm3	$$⊢\mathrm{dom}B=\left\{y|\exists w⟨y,w⟩\in B\right\}$$
9	8	csbeq2i	$$⊢⦋A/x⦌\mathrm{dom}B=⦋A/x⦌\left\{y|\exists w⟨y,w⟩\in B\right\}$$
10		dfdm3	$$⊢\mathrm{dom}⦋A/x⦌B=\left\{y|\exists w⟨y,w⟩\in ⦋A/x⦌B\right\}$$
11	7 9 10	3eqtr4i	$$⊢⦋A/x⦌\mathrm{dom}B=\mathrm{dom}⦋A/x⦌B$$