Theorem vtoclf

Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar . (Contributed by NM, 30-Aug-1993)

	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	2	isseti	$$⊢\exists xx=A$$
6	3	biimpd	$$⊢x=A\to \left(\phi \to \psi \right)$$
7	5 6	eximii	$$⊢\exists x\left(\phi \to \psi \right)$$
8	1 7	19.36i	$$⊢\forall x\phi \to \psi$$
9	8 4	mpg	$$⊢\psi$$