Theorem vtoclf

Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar . (Contributed by NM, 30-Aug-1993) (Proof shortened by Wolf Lammen, 26-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		vtoclf.1	|- F/ x ps
2		vtoclf.2	|- A e. _V
3		vtoclf.3	|- ( x = A -> ( ph <-> ps ) )
4		vtoclf.4	|- ph
5	4 3	mpbii	|- ( x = A -> ps )
6	1 2 5	vtoclef	|- ps