Theorem vtoclef

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

	Ref	Expression
Hypotheses	vtoclef.1	$$⊢Ⅎx\phi$$
	vtoclef.2	$$⊢A\in \mathrm{V}$$
	vtoclef.3	$$⊢x=A\to \phi$$
Assertion	vtoclef	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		vtoclef.1	$$⊢Ⅎx\phi$$
2		vtoclef.2	$$⊢A\in \mathrm{V}$$
3		vtoclef.3	$$⊢x=A\to \phi$$
4	2	isseti	$$⊢\exists xx=A$$
5	1 3	exlimi	$$⊢\exists xx=A\to \phi$$
6	4 5	ax-mp	$$⊢\phi$$