Theorem vtocl

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993) Remove dependency on ax-10 . (Revised by BJ, 29-Nov-2020) (Proof shortened by SN, 20-Apr-2024) (Proof shortened by Wolf Lammen, 20-Jun-2025)

	Ref	Expression
Hypotheses	vtocl.1	|- A e. _V
	vtocl.2	|- ( x = A -> ( ph <-> ps ) )
	vtocl.3	|- ph
Assertion	vtocl	|- ps

Proof

Step	Hyp	Ref	Expression
1		vtocl.1	|- A e. _V
2		vtocl.2	|- ( x = A -> ( ph <-> ps ) )
3		vtocl.3	|- ph
4	3 2	mpbii	|- ( x = A -> ps )
5	1 4	vtocle	|- ps