Theorem vtoclgf

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003) (Proof shortened by Mario Carneiro, 10-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		vtoclgf.1	|- F/_ x A
2		vtoclgf.2	|- F/ x ps
3		vtoclgf.3	|- ( x = A -> ( ph <-> ps ) )
4		vtoclgf.4	|- ph
5		elex	|- ( A e. V -> A e. _V )
6	1	issetf	|- ( A e. _V <-> E. x x = A )
7	4 3	mpbii	|- ( x = A -> ps )
8	2 7	exlimi	|- ( E. x x = A -> ps )
9	6 8	sylbi	|- ( A e. _V -> ps )
10	5 9	syl	|- ( A e. V -> ps )