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

Theorem vvex 4109
Description: The universal class exists. This marks a major departure from ZFC set theory, where is a proper class. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
vvex

Proof of Theorem vvex
StepHypRef Expression
1 uncompl 4074 . 2
2 vex 2862 . . 3
32complex 4104 . . 3
42, 3unex 4106 . 2
51, 4eqeltrri 2424 1
Colors of variables: wff set class
Syntax hints:   wcel 1710  cvv 2859   ∼ ccompl 3205   cun 3207
This theorem is referenced by:  0ex  4110  cnvkexg  4286  uni1exg  4292  ssetkex  4294  imakexg  4299  pw1exg  4302  ins2kexg  4305  ins3kexg  4306  cokexg  4309  imagekexg  4311  abexv  4324  pwexg  4328  nnsucelrlem1  4423  preaddccan1lem1  4453  ltfinex  4464  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  tfinrelkex  4487  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  srelkex  4525  tfinnnlem1  4533  vfinspnn  4541  1cvsfin  4542  tncveqnc1fin  4544  vfintle  4546  vfinncvntnn  4548  phiexg  4571  opexg  4587  proj1exg  4591  proj2exg  4592  setconslem5  4727  1stex  4731  swapex  4734  ssetex  4736  imaexg  4738  coexg  4741  siexg  4744  rnexg  5137  resexg  5149  ins2exg  5824  ins3exg  5825  imageexg  5829  mptexlem  5842  mpt2exlem  5843  cupex  5848  disjex  5851  addcfnex  5852  funsex  5856  fnsex  5858  crossex  5876  transex  5930  refex  5931  antisymex  5932  connexex  5933  foundex  5934  extex  5935  symex  5936  ider  5963  ssetpov  5964  eqer  5981  enex  6052  ener  6060  enpw1lem1  6081  enmap2lem1  6083  enmap1lem1  6089  enpw  6107  ncsex  6131  ncpw1c  6175  1p1e2c  6176  2p1e3c  6177  ce0addcnnul  6200  ce2  6213  ce2nc1  6214  lecncvg  6220  tcncv  6246  tcfnex  6264  nmembers1lem1  6272  nncdiv3lem2  6276  spacvallem1  6281  nchoicelem11  6299  nchoicelem19  6307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-un 3214
  Copyright terms: Public domain W3C validator