vnex - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem vnex 2705

Description: The universal class does not exist.

**Assertion**
Ref	Expression
vnex

**Proof of Theorem vnex**
Step	Hyp	Ref	Expression
1		nvelv 2703	. 2
2		isset 1805	. 2
3	1, 2	mtbi 191	1

Colors of variables: wff set class

Syntax hints:

wn 2

wceq 953

wcel 955

wex 977

cvv 1802

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 960 ax-8 961 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-ext 1452 ax-sep 2693

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-v 1803