Theorem csbief

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypotheses	csbief.1	$$⊢A\in \mathrm{V}$$
	csbief.2	$$⊢\underset{\_}{Ⅎ}xC$$
	csbief.3	$$⊢x=A\to B=C$$
Assertion	csbief	$$⊢⦋A/x⦌B=C$$

Proof

Step	Hyp	Ref	Expression
1		csbief.1	$$⊢A\in \mathrm{V}$$
2		csbief.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		csbief.3	$$⊢x=A\to B=C$$
4	2	a1i	$$⊢A\in \mathrm{V}\to \underset{\_}{Ⅎ}xC$$
5	4 3	csbiegf	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B=C$$
6	1 5	ax-mp	$$⊢⦋A/x⦌B=C$$