Theorem vtoclef

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993)

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

Proof

Step	Hyp	Ref	Expression
1		vtoclef.1	|- F/ x ph
2		vtoclef.2	|- A e. _V
3		vtoclef.3	|- ( x = A -> ph )
4	2	isseti	|- E. x x = A
5	1 3	exlimi	|- ( E. x x = A -> ph )
6	4 5	ax-mp	|- ph