Theorem csbie

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	csbie.1	|- A e. _V
	csbie.2	|- ( x = A -> B = C )
Assertion	csbie	|- [_ A / x ]_ B = C

Proof

Step	Hyp	Ref	Expression
1		csbie.1	|- A e. _V
2		csbie.2	|- ( x = A -> B = C )
3		nfcv	|- F/_ x C
4	1 3 2	csbief	|- [_ A / x ]_ B = C