Theorem vtoclefex

Description: Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Hypotheses	vtoclefex.1	$$⊢Ⅎx\phi$$
	vtoclefex.3	$$⊢x=A\to \phi$$
Assertion	vtoclefex	$$⊢A\in V\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		vtoclefex.1	$$⊢Ⅎx\phi$$
2		vtoclefex.3	$$⊢x=A\to \phi$$
3	2	ax-gen	$$⊢\forall x\left(x=A\to \phi \right)$$
4		vtoclegft	$$⊢\left(A\in V\wedge Ⅎx\phi \wedge \forall x\left(x=A\to \phi \right)\right)\to \phi$$
5	1 3 4	mp3an23	$$⊢A\in V\to \phi$$