Theorem vtoclefex

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

	Ref	Expression
Hypotheses	vtoclefex.1	|- F/ x ph
	vtoclefex.3	|- ( x = A -> ph )
Assertion	vtoclefex	|- ( A e. V -> ph )

Proof

Step	Hyp	Ref	Expression
1		vtoclefex.1	|- F/ x ph
2		vtoclefex.3	|- ( x = A -> ph )
3	2	ax-gen	|- A. x ( x = A -> ph )
4		vtoclegft	|- ( ( A e. V /\ F/ x ph /\ A. x ( x = A -> ph ) ) -> ph )
5	1 3 4	mp3an23	|- ( A e. V -> ph )