NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  vvex Unicode version

Theorem vvex 3211
Description: The universal class exists. This marks a major departure from ZFC set theory, where is a proper class.
Assertion
Ref Expression
vvex

Proof of Theorem vvex
StepHypRef Expression
1 uncompl 2769 . 2
2 vex 2303 . . 3
32complex 3206 . . 3
42, 3unex 3208 . 2
51, 4eqeltrri 1965 1
Colors of variables: wff set class
Syntax hints:   wcel 1400  cvv 2300   ∼ ccompl 2607   cun 2609
This theorem is referenced by:  0ex  3212  cnvkexg  3390  uni1exg  3396  ssetkex  3398  imakexg  3403  pw1exg  3406  ins2kexg  3409  ins3kexg  3410  cokexg  3413  imagekexg  3415  abexv  3434  pwexg  3438  nnsucelrlem1  3531  preaddccan1lem1  3561  ltfinex  3572  ssfin  3578  ncfinraiselem2  3588  ncfinlowerlem1  3590  tfinrelkex  3595  evenfinex  3611  oddfinex  3612  evenodddisjlem1  3623  nnadjoinlem1  3627  srelkex  3633  tfinnnlem1  3641  vfinspnn  3649  1cvsfin  3650  tncveqnc1fin  3652  vfintle  3654  vfinncvntnn  3656  phiexg  3679  opexg  3695  proj1exg  3699  proj2exg  3700  setconslem5  3833  1stex  3837  swapex  3840  ssetex  3842  imaexg  3844  coexg  3847  siexg  3850  rnexg  4314  resexg  4326  ins2exg  5015  ins3exg  5016  imageexg  5020  mptexlem  5033  mpt2exlem  5034  cupex  5039  disjex  5042  addcfnex  5043  funsex  5047  fnsex  5049  crossex  5067  transex  5121  refex  5122  antisymex  5123  connexex  5124  foundex  5125  extex  5126  symex  5127  ider  5154  ssetpov  5155  eqer  5172  enex  5244  ener  5252  enpw1lem1  5273  enmap2lem1  5275  enmap1lem1  5281  enpw  5299  ncsex  5323  ncpw1c  5367  1p1e2c  5368  2p1e3c  5369  ce0addcnnul  5392  ce2  5405  ce2nc1  5406  lecncvg  5412  tcncv  5438  tcfnex  5456  nmembers1lem1  5464  nncdiv3lem2  5468  spacvallem1  5473  nchoicelem11  5491  nchoicelem19  5499
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-17 1413  ax-9 1424  ax-4 1429  ax-16 1606  ax-ext 1877  ax-nin 3180
This theorem depends on definitions:  df-bi 174  df-or 356  df-an 357  df-nand 1259  df-ex 1328  df-sb 1568  df-clab 1883  df-cleq 1888  df-clel 1891  df-ne 2014  df-v 2302  df-nin 2613  df-compl 2614  df-in 2615  df-un 2616  df-nul 2727
  Copyright terms: Public domain W3C validator