MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ex Unicode version

Theorem 0ex 4150
Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 4149. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex  |-  (/)  e.  _V

Proof of Theorem 0ex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 4149 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3469 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1569 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 200 . 2  |-  E. x  x  =  (/)
54issetri 2795 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788   (/)c0 3455
This theorem is referenced by:  class2set  4178  0elpw  4180  0nep0  4181  unidif0  4183  iin0  4184  notzfaus  4185  intv  4186  snexALT  4196  p0ex  4197  dtruALT  4207  zfpair  4212  snex  4216  dtruALT2  4219  opex  4237  opthwiener  4268  0elon  4445  nsuceq0  4472  snsn0non  4511  unisn2  4522  onint0  4587  tfinds2  4654  finds  4682  finds2  4684  opthprc  4736  xpexr  5114  soex  5122  dmsnsnsn  5151  iotaex  5236  nfunv  5285  fun0  5307  fvrn0  5550  fvssunirn  5551  brtpos0  6241  reldmtpos  6242  tfrlem16  6409  tz7.44-1  6419  seqomlem1  6462  1n0  6494  el1o  6498  om0  6516  map0e  6805  ixpexg  6840  0elixp  6847  en0  6924  ensn1  6925  en1  6928  2dom  6933  map1  6939  xp1en  6948  endisj  6949  pw2eng  6968  map2xp  7031  limensuci  7037  1sdom  7065  unxpdom2  7071  sucxpdom  7072  isinf  7076  ac6sfi  7101  fodomfi  7135  fi0  7173  oiexg  7250  brwdom  7281  brwdom2  7287  inf3lemb  7326  infeq5i  7337  dfom3  7348  cantnfvalf  7366  cantnfval2  7370  cantnflt  7373  cantnff  7375  cantnf0  7376  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem1  7391  cantnf  7395  cnfcom  7403  tc0  7432  r10  7440  scottex  7555  infxpenlem  7641  fseqenlem1  7651  dfac9  7762  uncdadom  7797  cdaun  7798  cdaen  7799  cda1dif  7802  pm110.643  7803  cda0en  7805  cdacomen  7807  cdaassen  7808  xpcdaen  7809  mapcdaen  7810  cdaxpdom  7815  cdainf  7818  infcda1  7819  pwsdompw  7830  pwcdadom  7842  ackbij1lem14  7859  ackbij2lem2  7866  ackbij2lem3  7867  cf0  7877  cfeq0  7882  cfsuc  7883  cflim2  7889  isfin5  7925  isfin4-3  7941  fin1a2lem11  8036  fin1a2lem12  8037  fin1a2lem13  8038  axcc2lem  8062  ac6num  8106  zornn0g  8132  ttukeylem3  8138  brdom3  8153  iundom2g  8162  cardeq0  8174  alephadd  8199  pwcfsdom  8205  axpowndlem3  8221  canthwe  8273  canthp1lem1  8274  pwxpndom2  8287  pwcdandom  8289  gchxpidm  8291  intwun  8357  0tsk  8377  grothomex  8451  indpi  8531  fzennn  11030  hash0  11355  hashmap  11387  hashbc  11391  hashf1  11395  swrdval  11450  swrd00  11451  incexclem  12295  incexc  12296  rexpen  12506  sadcf  12644  sadc0  12645  sadcp1  12646  smupf  12669  smup0  12670  smupp1  12671  0ram  13067  ram0  13069  str0  13184  ressbas  13198  ress0  13202  0rest  13334  xpscg  13460  xpscfn  13461  xpsc0  13462  xpsc1  13463  xpsfrnel  13465  xpsfrnel2  13467  xpsle  13483  ismred2  13505  acsfn  13561  0cat  13590  setcepi  13920  0pos  14088  meet0  14241  join0  14242  gsum0  14457  ga0  14752  oppglsm  14953  efgi0  15029  vrgpf  15077  vrgpinv  15078  frgpuptinv  15080  frgpup2  15085  0frgp  15088  frgpnabllem1  15161  frgpnabllem2  15162  dprd0  15266  dmdprdpr  15284  dprdpr  15285  00lsp  15738  fvcoe1  16288  coe1f2  16290  coe1sfi  16293  coe1add  16341  coe1mul2lem1  16344  coe1mul2lem2  16345  coe1mul2  16346  ply1coe  16368  frgpcyg  16527  topgele  16672  en1top  16722  en2top  16723  sn0topon  16735  indistopon  16738  indistps  16748  indistps2  16749  sn0cld  16827  indiscld  16828  rest0  16900  restsn  16901  cmpfi  17135  txindislem  17327  hmphindis  17488  xpstopnlem1  17500  xpstopnlem2  17502  ptcmpfi  17504  snfil  17559  fbasfip  17563  fgcl  17573  filcon  17578  fbasrn  17579  filuni  17580  cfinfil  17588  csdfil  17589  supfil  17590  ufildr  17626  fin1aufil  17627  rnelfmlem  17647  fclsval  17703  tmdgsum  17778  tsmsfbas  17810  0met  17930  xpsdsval  17945  minveclem3b  18792  evl1rhm  19412  evl1sca  19413  evl1var  19415  pf1mpf  19435  pf1ind  19438  tdeglem2  19447  deg1ldg  19478  deg1leb  19481  deg1val  19482  ulm0  19770  disjdifprg  23352  esumnul  23427  prsiga  23492  derang0  23700  indispcon  23765  umgra0  23877  vdgr0  23892  rdgprc  24151  dfrdg3  24153  trpredpred  24231  trpred0  24239  nosgnn0  24312  nodense  24343  fullfunfnv  24484  fullfunfv  24485  rank0  24800  ssoninhaus  24887  onint1  24888  alexeqd  24962  vxveqv  25054  ac5g  25075  snelpwg  25091  ab2rexexg  25122  fprg  25133  empos  25242  fisub  25554  0alg  25756  0ded  25757  0catOLD  25758  selsubf3g  25992  isconc1  26006  isconc2  26007  heibor1lem  26533  heiborlem6  26540  reheibor  26563  prter2  26749  mzpcompact2lem  26829  wopprc  27123  pw2f1ocnv  27130  pwslnmlem0  27193  fnchoice  27700  afv0fv0  28012  usgra0  28116  usgra0v  28117  cusgra0v  28156  cusgra1v  28157  uvtx01vtx  28164  frgra0v  28174  bnj941  28804  bnj97  28898  bnj149  28907  bnj150  28908  bnj944  28970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator