Theorem vtoclgaf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	vtoclgaf.1	|- F/_ x A
	vtoclgaf.2	|- F/ x ps
	vtoclgaf.3	|- ( x = A -> ( ph <-> ps ) )
	vtoclgaf.4	|- ( x e. B -> ph )
Assertion	vtoclgaf	|- ( A e. B -> ps )

Proof

Step	Hyp	Ref	Expression
1		vtoclgaf.1	|- F/_ x A
2		vtoclgaf.2	|- F/ x ps
3		vtoclgaf.3	|- ( x = A -> ( ph <-> ps ) )
4		vtoclgaf.4	|- ( x e. B -> ph )
5	1	nfel1	|- F/ x A e. B
6	5 2	nfim	|- F/ x ( A e. B -> ps )
7		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
8	7 3	imbi12d	|- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	1 6 8 4	vtoclgf	|- ( A e. B -> ( A e. B -> ps ) )
10	9	pm2.43i	|- ( A e. B -> ps )