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

Theorem 0ex 4166
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 4165. (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 4165 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3482 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1572 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 200 . 2  |-  E. x  x  =  (/)
54issetri 2808 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468
This theorem is referenced by:  class2set  4194  0elpw  4196  0nep0  4197  unidif0  4199  iin0  4200  notzfaus  4201  intv  4202  snexALT  4212  p0ex  4213  dtruALT  4223  zfpair  4228  snex  4232  dtruALT2  4235  opex  4253  opthwiener  4284  0elon  4461  nsuceq0  4488  snsn0non  4527  unisn2  4538  onint0  4603  tfinds2  4670  finds  4698  finds2  4700  opthprc  4752  xpexr  5130  soex  5138  dmsnsnsn  5167  iotaex  5252  nfunv  5301  fun0  5323  fvrn0  5566  fvssunirn  5567  brtpos0  6257  reldmtpos  6258  tfrlem16  6425  tz7.44-1  6435  seqomlem1  6478  1n0  6510  el1o  6514  om0  6532  map0e  6821  ixpexg  6856  0elixp  6863  en0  6940  ensn1  6941  en1  6944  2dom  6949  map1  6955  xp1en  6964  endisj  6965  pw2eng  6984  map2xp  7047  limensuci  7053  1sdom  7081  unxpdom2  7087  sucxpdom  7088  isinf  7092  ac6sfi  7117  fodomfi  7151  fi0  7189  oiexg  7266  brwdom  7297  brwdom2  7303  inf3lemb  7342  infeq5i  7353  dfom3  7364  cantnfvalf  7382  cantnfval2  7386  cantnflt  7389  cantnff  7391  cantnf0  7392  cantnfp1lem3  7398  cantnflem1d  7406  cantnflem1  7407  cantnf  7411  cnfcom  7419  tc0  7448  r10  7456  scottex  7571  infxpenlem  7657  fseqenlem1  7667  dfac9  7778  uncdadom  7813  cdaun  7814  cdaen  7815  cda1dif  7818  pm110.643  7819  cda0en  7821  cdacomen  7823  cdaassen  7824  xpcdaen  7825  mapcdaen  7826  cdaxpdom  7831  cdainf  7834  infcda1  7835  pwsdompw  7846  pwcdadom  7858  ackbij1lem14  7875  ackbij2lem2  7882  ackbij2lem3  7883  cf0  7893  cfeq0  7898  cfsuc  7899  cflim2  7905  isfin5  7941  isfin4-3  7957  fin1a2lem11  8052  fin1a2lem12  8053  fin1a2lem13  8054  axcc2lem  8078  ac6num  8122  zornn0g  8148  ttukeylem3  8154  brdom3  8169  iundom2g  8178  cardeq0  8190  alephadd  8215  pwcfsdom  8221  axpowndlem3  8237  canthwe  8289  canthp1lem1  8290  pwxpndom2  8303  pwcdandom  8305  gchxpidm  8307  intwun  8373  0tsk  8393  grothomex  8467  indpi  8547  fzennn  11046  hash0  11371  hashmap  11403  hashbc  11407  hashf1  11411  swrdval  11466  swrd00  11467  incexclem  12311  incexc  12312  rexpen  12522  sadcf  12660  sadc0  12661  sadcp1  12662  smupf  12685  smup0  12686  smupp1  12687  0ram  13083  ram0  13085  str0  13200  ressbas  13214  ress0  13218  0rest  13350  xpscg  13476  xpscfn  13477  xpsc0  13478  xpsc1  13479  xpsfrnel  13481  xpsfrnel2  13483  xpsle  13499  ismred2  13521  acsfn  13577  0cat  13606  setcepi  13936  0pos  14104  meet0  14257  join0  14258  gsum0  14473  ga0  14768  oppglsm  14969  efgi0  15045  vrgpf  15093  vrgpinv  15094  frgpuptinv  15096  frgpup2  15101  0frgp  15104  frgpnabllem1  15177  frgpnabllem2  15178  dprd0  15282  dmdprdpr  15300  dprdpr  15301  00lsp  15754  fvcoe1  16304  coe1f2  16306  coe1sfi  16309  coe1add  16357  coe1mul2lem1  16360  coe1mul2lem2  16361  coe1mul2  16362  ply1coe  16384  frgpcyg  16543  topgele  16688  en1top  16738  en2top  16739  sn0topon  16751  indistopon  16754  indistps  16764  indistps2  16765  sn0cld  16843  indiscld  16844  rest0  16916  restsn  16917  cmpfi  17151  txindislem  17343  hmphindis  17504  xpstopnlem1  17516  xpstopnlem2  17518  ptcmpfi  17520  snfil  17575  fbasfip  17579  fgcl  17589  filcon  17594  fbasrn  17595  filuni  17596  cfinfil  17604  csdfil  17605  supfil  17606  ufildr  17642  fin1aufil  17643  rnelfmlem  17663  fclsval  17719  tmdgsum  17794  tsmsfbas  17826  0met  17946  xpsdsval  17961  minveclem3b  18808  evl1rhm  19428  evl1sca  19429  evl1var  19431  pf1mpf  19451  pf1ind  19454  tdeglem2  19463  deg1ldg  19494  deg1leb  19497  deg1val  19498  ulm0  19786  disjdifprg  23367  esumnul  23442  prsiga  23507  derang0  23715  indispcon  23780  umgra0  23892  vdgr0  23907  rdgprc  24222  dfrdg3  24224  trpredpred  24302  trpred0  24310  nosgnn0  24383  nodense  24414  fullfunfnv  24556  fullfunfv  24557  rank0  24872  ssoninhaus  24959  onint1  24960  alexeqd  25065  vxveqv  25157  ac5g  25178  snelpwg  25194  ab2rexexg  25225  fprg  25236  empos  25345  fisub  25657  0alg  25859  0ded  25860  0catOLD  25861  selsubf3g  26095  isconc1  26109  isconc2  26110  heibor1lem  26636  heiborlem6  26643  reheibor  26666  prter2  26852  mzpcompact2lem  26932  wopprc  27226  pw2f1ocnv  27233  pwslnmlem0  27296  fnchoice  27803  afv0fv0  28117  usgra0  28250  usgra0v  28251  cusgra0v  28295  cusgra1v  28296  uvtx01vtx  28305  0wlk  28343  0trl  28344  0pth  28356  0spth  28357  0crct  28371  0cycl  28372  frgra0v  28420  bnj941  29120  bnj97  29214  bnj149  29223  bnj150  29224  bnj944  29286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator