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	|- F/ x ph
	csbiedf.2	|- ( ph -> F/_ x C )
	csbiedf.3	|- ( ph -> A e. V )
	csbiedf.4	|- ( ( ph /\ x = A ) -> B = C )
Assertion	csbiedf	|- ( ph -> [_ A / x ]_ B = C )

Proof

Step	Hyp	Ref	Expression
1		csbiedf.1	|- F/ x ph
2		csbiedf.2	|- ( ph -> F/_ x C )
3		csbiedf.3	|- ( ph -> A e. V )
4		csbiedf.4	|- ( ( ph /\ x = A ) -> B = C )
5	4	ex	|- ( ph -> ( x = A -> B = C ) )
6	1 5	alrimi	|- ( ph -> A. x ( x = A -> B = C ) )
7		csbiebt	|- ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
8	3 2 7	syl2anc	|- ( ph -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
9	6 8	mpbid	|- ( ph -> [_ A / x ]_ B = C )