Theorem vnex

Description: The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005)

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

Proof

Step	Hyp	Ref	Expression
1		nalset	$$⊢\neg \exists x\forall yy\in x$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	tbt	$$⊢y\in x\leftrightarrow \left(y\in x\leftrightarrow y\in \mathrm{V}\right)$$
4	3	albii	$$⊢\forall yy\in x\leftrightarrow \forall y\left(y\in x\leftrightarrow y\in \mathrm{V}\right)$$
5		dfcleq	$$⊢x=\mathrm{V}\leftrightarrow \forall y\left(y\in x\leftrightarrow y\in \mathrm{V}\right)$$
6	4 5	bitr4i	$$⊢\forall yy\in x\leftrightarrow x=\mathrm{V}$$
7	6	exbii	$$⊢\exists x\forall yy\in x\leftrightarrow \exists xx=\mathrm{V}$$
8	1 7	mtbi	$$⊢\neg \exists xx=\mathrm{V}$$