Theorem vtocleg

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

	Ref	Expression
Hypothesis	vtocleg.1	$$⊢x=A\to \phi$$
Assertion	vtocleg	$$⊢A\in V\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		vtocleg.1	$$⊢x=A\to \phi$$
2		elisset	$$⊢A\in V\to \exists xx=A$$
3	1	exlimiv	$$⊢\exists xx=A\to \phi$$
4	2 3	syl	$$⊢A\in V\to \phi$$