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	$$⊢Ⅎx\psi$$
	vtoclf.2	$$⊢A\in \mathrm{V}$$
	vtoclf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtoclf.4	$$⊢\phi$$
Assertion	vtoclf	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		vtoclf.1	$$⊢Ⅎx\psi$$
2		vtoclf.2	$$⊢A\in \mathrm{V}$$
3		vtoclf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		vtoclf.4	$$⊢\phi$$
5	4 3	mpbii	$$⊢x=A\to \psi$$
6	1 2 5	vtoclef	$$⊢\psi$$