Theorem vtocle

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

	Ref	Expression
Hypotheses	vtocle.1	|- A e. _V
	vtocle.2	|- ( x = A -> ph )
Assertion	vtocle	|- ph

Proof

Step	Hyp	Ref	Expression
1		vtocle.1	|- A e. _V
2		vtocle.2	|- ( x = A -> ph )
3	2	vtocleg	|- ( A e. _V -> ph )
4	1 3	ax-mp	|- ph