Theorem csbeq2d

Description: Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	csbeq2d.1	$$⊢Ⅎx\phi$$
	csbeq2d.2	$$⊢\phi \to B=C$$
Assertion	csbeq2d	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		csbeq2d.1	$$⊢Ⅎx\phi$$
2		csbeq2d.2	$$⊢\phi \to B=C$$
3	2	eleq2d	$$⊢\phi \to \left(y\in B\leftrightarrow y\in C\right)$$
4	1 3	sbcbid	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)$$
5	4	abbidv	$$⊢\phi \to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
6		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
7		df-csb	$$⊢⦋A/x⦌C=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
8	5 6 7	3eqtr4g	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$