vnex

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

		Ref	Expression
	Assertion	vnex	$⊢ \neg \exists x x = V$

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

Metamath Proof Explorer