Theorem vnex

Description: The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005) (Proof shortened by BJ, 25-Apr-2026)

	Ref	Expression
Assertion	vnex	$$⊢\neg \exists xx=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vneqv	$$⊢\neg x=\mathrm{V}$$
2	1	nex	$$⊢\neg \exists xx=\mathrm{V}$$