Theorem sbciegf

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

	Ref	Expression
Hypotheses	sbciegf.1	|- F/ x ps
	sbciegf.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	sbciegf	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbciegf.1	|- F/ x ps
2		sbciegf.2	|- ( x = A -> ( ph <-> ps ) )
3	2	ax-gen	|- A. x ( x = A -> ( ph <-> ps ) )
4		sbciegft	|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )
5	1 3 4	mp3an23	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )