Theorem vneqv

Description: The universal class is not equal to any setvar. (Contributed by NM, 4-Jul-2005) Extract from vnex and shorten proof. (Revised by BJ, 25-Apr-2026)

	Ref	Expression
Assertion	vneqv	$$⊢\neg x=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		eleq2	$$⊢x=\mathrm{V}\to \left(y\in x\leftrightarrow y\in \mathrm{V}\right)$$
3	1 2	mpbiri	$$⊢x=\mathrm{V}\to y\in x$$
4	3	con3i	$$⊢\neg y\in x\to \neg x=\mathrm{V}$$
5		exnelv	$$⊢\exists y\neg y\in x$$
6	4 5	exlimiiv	$$⊢\neg x=\mathrm{V}$$