Theorem csbie

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024)

	Ref	Expression
Hypotheses	csbie.1	$$⊢A\in \mathrm{V}$$
	csbie.2	$$⊢x=A\to B=C$$
Assertion	csbie	$$⊢⦋A/x⦌B=C$$

Proof

Step	Hyp	Ref	Expression
1		csbie.1	$$⊢A\in \mathrm{V}$$
2		csbie.2	$$⊢x=A\to B=C$$
3		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
4	2	eleq2d	$$⊢x=A\to \left(y\in B\leftrightarrow y\in C\right)$$
5	1 4	sbcie	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in C$$
6	5	abbii	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|y\in C\right\}$$
7		abid2	$$⊢\left\{y|y\in C\right\}=C$$
8	3 6 7	3eqtri	$$⊢⦋A/x⦌B=C$$