Theorem csbeq1

Description: Analogue of dfsbcq for proper substitution into a class. (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbeq1	$$⊢A=B\to ⦋A/x⦌C=⦋B/x⦌C$$

Proof

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