Theorem vtoclf

Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar . (Contributed by NM, 30-Aug-1993)

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

Proof

Step	Hyp	Ref	Expression
1		vtoclf.1	|- F/ x ps
2		vtoclf.2	|- A e. _V
3		vtoclf.3	|- ( x = A -> ( ph <-> ps ) )
4		vtoclf.4	|- ph
5	2	isseti	|- E. x x = A
6	3	biimpd	|- ( x = A -> ( ph -> ps ) )
7	5 6	eximii	|- E. x ( ph -> ps )
8	1 7	19.36i	|- ( A. x ph -> ps )
9	8 4	mpg	|- ps