Theorem csbiegf

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

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

Proof

Step	Hyp	Ref	Expression
1		csbiegf.1	$$⊢A\in V\to \underset{\_}{Ⅎ}xC$$
2		csbiegf.2	$$⊢x=A\to B=C$$
3	2	ax-gen	$$⊢\forall x\left(x=A\to B=C\right)$$
4		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)$$
5	1 4	mpdan	$$⊢A\in V\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
6	3 5	mpbii	$$⊢A\in V\to ⦋A/x⦌B=C$$