Theorem csbeq2dv

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

	Ref	Expression
Hypothesis	csbeq2dv.1	$$⊢\phi \to B=C$$
Assertion	csbeq2dv	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		csbeq2dv.1	$$⊢\phi \to B=C$$
2	1	eleq2d	$$⊢\phi \to \left(y\in B\leftrightarrow y\in C\right)$$
3	2	sbcbidv	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)$$
4	3	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\}$$
5		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
6		df-csb	$$⊢⦋A/x⦌C=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
7	4 5 6	3eqtr4g	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$