Theorem csbeq2

Description: Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018)

	Ref	Expression
Assertion	csbeq2	$$⊢\forall xB=C\to ⦋A/x⦌B=⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢B=C\to \left(y\in B\leftrightarrow y\in C\right)$$
2	1	alimi	$$⊢\forall xB=C\to \forall x\left(y\in B\leftrightarrow y\in C\right)$$
3		sbcbi2	$$⊢\forall x\left(y\in B\leftrightarrow y\in C\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)$$
4	2 3	syl	$$⊢\forall xB=C\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	$$⊢\forall xB=C\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	$$⊢\forall xB=C\to ⦋A/x⦌B=⦋A/x⦌C$$