Theorem csbiedf

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

	Ref	Expression
Hypotheses	csbiedf.1	$$⊢Ⅎx\phi$$
	csbiedf.2	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$
	csbiedf.3	$$⊢\phi \to A\in V$$
	csbiedf.4	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
Assertion	csbiedf	$$⊢\phi \to ⦋A/x⦌B=C$$

Proof

Step	Hyp	Ref	Expression
1		csbiedf.1	$$⊢Ⅎx\phi$$
2		csbiedf.2	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$
3		csbiedf.3	$$⊢\phi \to A\in V$$
4		csbiedf.4	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
5	4	ex	$$⊢\phi \to \left(x=A\to B=C\right)$$
6	1 5	alrimi	$$⊢\phi \to \forall x\left(x=A\to B=C\right)$$
7		csbiebt	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
8	3 2 7	syl2anc	$$⊢\phi \to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
9	6 8	mpbid	$$⊢\phi \to ⦋A/x⦌B=C$$