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

Theorem 0ex 4432
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 4431. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex

Proof of Theorem 0ex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 4431 . . 3
2 eq0 3674 . . . 4
32exbii 1601 . . 3
41, 3mpbir 202 . 2
54issetri 3013 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  A.wal 1556  E.wex 1557  =wceq 1662  e.wcel 1724   cvv 3006   c0 3660
This theorem is referenced by:  sseliALT  4433  csbexg  4434  unisn2  4438  class2set  4466  0elpw  4468  0nep0  4470  unidif0  4472  iin0  4473  notzfaus  4474  intv  4475  snexALT  4485  p0ex  4486  dtruALT  4531  zfpair  4536  snex  4540  dtruALT2  4543  opex  4563  opthwiener  4597  0elon  4775  nsuceq0  4802  snsn0non  4841  opthprc  4890  dmsnsnsn  5316  iotaex  5397  nfunv  5448  fun0  5472  fvrn0  5706  fvssunirn  5707  fprg  5877  onint0  6372  tfinds2  6439  finds  6467  finds2  6469  xpexr  6482  soex  6484  brtpos0  6669  reldmtpos  6670  tfrlem16  6766  tz7.44-1  6776  seqomlem1  6819  1n0  6851  el1o  6855  om0  6873  map0e  7163  ixpexg  7198  0elixp  7205  en0  7282  ensn1  7283  en1  7286  2dom  7291  map1  7297  xp1en  7306  endisj  7307  pw2eng  7326  map2xp  7389  limensuci  7395  1sdom  7423  unxpdom2  7429  sucxpdom  7430  isinf  7434  ac6sfi  7463  fodomfi  7497  fi0  7537  oiexg  7616  brwdom  7647  brwdom2  7653  inf3lemb  7692  infeq5i  7703  dfom3  7714  cantnfvalf  7732  cantnfval2  7736  cantnflt  7739  cantnff  7741  cantnf0  7742  cantnfp1lem3  7748  cantnflem1d  7756  cantnflem1  7757  cantnf  7761  cnfcom  7769  tc0  7798  r10  7806  scottex  7923  infxpenlem  8009  fseqenlem1  8019  uncdadom  8165  cdaun  8166  cdaen  8167  cda1dif  8170  pm110.643  8171  cda0en  8173  cdacomen  8175  cdaassen  8176  xpcdaen  8177  mapcdaen  8178  cdaxpdom  8183  cdainf  8186  infcda1  8187  pwsdompw  8198  pwcdadom  8210  ackbij1lem14  8227  ackbij2lem2  8234  ackbij2lem3  8235  cf0  8245  cfeq0  8250  cfsuc  8251  cflim2  8257  isfin5  8293  isfin4-3  8309  fin1a2lem11  8404  fin1a2lem12  8405  fin1a2lem13  8406  axcc2lem  8430  ac6num  8473  zornn0g  8499  ttukeylem3  8505  brdom3  8520  iundom2g  8529  cardeq0  8541  alephadd  8566  pwcfsdom  8572  axpowndlem3  8588  canthwe  8640  canthp1lem1  8641  pwxpndom2  8654  pwcdandom  8656  gchxpidm  8658  intwun  8724  0tsk  8744  grothomex  8818  indpi  8898  fzennn  11582  hash0  11927  hashmap  11984  hashbc  11993  hashf1  11997  swrdval  12100  swrd00  12101  swrd0  12114  cshfn  12213  cshnz  12215  0csh0  12216  incexclem  13085  incexc  13086  rexpen  13296  sadcf  13435  sadc0  13436  sadcp1  13437  smupf  13460  smup0  13461  smupp1  13462  0ram  13867  ram0  13869  cshws0  13914  str0  13996  ressbas  14010  ress0  14014  0rest  14148  xpscg  14274  xpscfn  14275  xpsc0  14276  xpsc1  14277  xpsfrnel  14279  xpsfrnel2  14281  xpsle  14297  ismred2  14319  acsfn  14375  0cat  14404  setcepi  14734  0pos  14902  meet0  15085  join0  15086  gsum0  15283  ga0  15578  oppglsm  15779  efgi0  15855  vrgpf  15903  vrgpinv  15904  frgpuptinv  15906  frgpup2  15911  0frgp  15914  frgpnabllem1  15987  frgpnabllem2  15988  dprd0  16092  dmdprdpr  16110  dprdpr  16111  00lsp  16560  fvcoe1  17108  coe1f2  17110  coe1sfi  17113  coe1add  17160  coe1mul2lem1  17163  coe1mul2lem2  17164  coe1mul2  17165  ply1coe  17187  frgpcyg  17357  topgele  17502  en1top  17552  en2top  17553  sn0topon  17565  indistopon  17568  indistps  17578  indistps2  17579  sn0cld  17657  indiscld  17658  neipeltop  17696  rest0  17736  restsn  17737  cmpfi  17974  txindislem  18169  hmphindis  18333  xpstopnlem1  18345  xpstopnlem2  18347  ptcmpfi  18349  snfil  18400  fbasfip  18404  fgcl  18414  filcon  18419  fbasrn  18420  cfinfil  18429  csdfil  18430  supfil  18431  ufildr  18467  fin1aufil  18468  rnelfmlem  18488  fclsval  18544  tmdgsum  18629  tsmsfbas  18661  ust0  18753  ustn0  18754  0met  18900  xpsdsval  18915  minveclem3b  19833  evl1rhm  20453  evl1sca  20454  evl1var  20456  pf1mpf  20476  pf1ind  20479  tdeglem2  20488  deg1ldg  20519  deg1leb  20522  deg1val  20523  ulm0  20811  uhgra0  21853  uhgra0v  21854  umgra0  21869  usgra0  21899  usgra0v  21900  cusgra0v  21978  cusgra1v  21979  uvtx01vtx  22010  0wlk  22054  0trl  22055  0wlkon  22056  0trlon  22057  0pth  22079  0spth  22080  0pthon  22088  0pthonv  22090  0crct  22122  0cycl  22123  0conngra  22170  vdgr0  22180  disjdifprg  24538  resvsca  24957  esumnul  25173  prsiga  25245  derang0  25694  indispcon  25760  rdgprc  26252  dfrdg3  26254  trpredpred  26336  trpred0  26344  nosgnn0  26443  nodense  26474  fullfunfnv  26621  fullfunfv  26622  rank0  26941  ssoninhaus  27028  onint1  27029  heibor1lem  27381  heiborlem6  27388  reheibor  27411  mzpcompact2lem  27739  wopprc  28030  pw2f1ocnv  28037  pwslnmlem0  28099  fnchoice  28601  afv0fv0  28911  0clwlk  29287  0egra0rgra  29408  0vgrargra  29409  frgra0v  29444  2spot0  29516  bnj941  30336  bnj97  30430  bnj149  30439  bnj150  30440  bnj944  30502  bj-eltag  30682  bj-tagss  30683  bj-xpnzex  30693  bj-pr1val  30703  bj-2upleex  30708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-nul 4431
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-v 3008  df-dif 3356  df-nul 3661
  Copyright terms: Public domain W3C validator