Theorem vtocle

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993) Avoid df-clab . (Revised by Wolf Lammen, 31-May-2025)

	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	1	isseti	|- E. x x = A
4	2 3	exlimiiv	|- ph