Theorem vtocl

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

	Ref	Expression
Hypotheses	vtocl.1	$$⊢A\in \mathrm{V}$$
	vtocl.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtocl.3	$$⊢\phi$$
Assertion	vtocl	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		vtocl.1	$$⊢A\in \mathrm{V}$$
2		vtocl.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		vtocl.3	$$⊢\phi$$
4	3 2	mpbii	$$⊢x=A\to \psi$$
5	1	isseti	$$⊢\exists xx=A$$
6	4 5	exlimiiv	$$⊢\psi$$