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

Theorem 0ex 4582
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 4581. (Contributed by NM, 21-Jun-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 4581 . . 3
2 eq0 3800 . . . 4
32exbii 1667 . . 3
41, 3mpbir 209 . 2
54issetri 3116 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109   c0 3784
This theorem is referenced by:  sseliALT  4583  csbexg  4584  unisn2  4588  class2set  4619  0elpw  4621  0nep0  4623  unidif0  4625  iin0  4626  notzfaus  4627  intv  4628  snexALT  4638  p0ex  4639  dtruALT  4684  zfpair  4689  snex  4693  dtruALT2  4696  opex  4716  opthwiener  4754  0elon  4936  nsuceq0  4963  snsn0non  5001  opthprc  5052  dmsnsnsn  5491  iotaex  5573  nfunv  5624  fun0  5650  fvrn0  5893  fvssunirn  5894  fprg  6080  ovima0  6454  onint0  6631  tfinds2  6698  finds  6726  finds2  6728  xpexr  6740  soex  6743  supp0  6923  fvn0elsupp  6934  fvn0elsuppOLD  6935  fvn0elsuppb  6936  brtpos0  6981  reldmtpos  6982  tfrlem16  7081  tz7.44-1  7091  seqomlem1  7134  1n0  7164  el1o  7168  om0  7186  map0e  7476  ixpexg  7513  0elixp  7520  en0  7598  ensn1  7599  en1  7602  2dom  7608  map1  7614  xp1en  7623  endisj  7624  pw2eng  7643  map2xp  7707  limensuci  7713  1sdom  7742  unxpdom2  7748  sucxpdom  7749  isinf  7753  ac6sfi  7784  fodomfi  7819  0fsupp  7871  fi0  7900  oiexg  7981  brwdom  8014  brwdom2  8020  inf3lemb  8063  infeq5i  8074  dfom3  8085  cantnffvalOLD  8103  cantnfvalf  8105  cantnfval2  8109  cantnfle  8111  cantnflt  8112  cantnff  8114  cantnf0  8115  cantnfp1lem1  8118  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnfp1  8121  cantnflem1a  8125  cantnflem1d  8128  cantnflem1  8129  cantnflem3  8131  cantnf  8133  cantnfval2OLD  8139  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnfOLD  8155  cnfcomlem  8164  cnfcom  8165  cnfcom2lem  8166  cnfcom3  8169  cnfcomOLD  8173  tc0  8199  r10  8207  scottex  8324  infxpenlem  8412  fseqenlem1  8426  uncdadom  8572  cdaun  8573  cdaen  8574  cda1dif  8577  pm110.643  8578  cda0en  8580  cdacomen  8582  cdaassen  8583  xpcdaen  8584  mapcdaen  8585  cdaxpdom  8590  cdainf  8593  infcda1  8594  pwsdompw  8605  pwcdadom  8617  ackbij1lem14  8634  ackbij2lem2  8641  ackbij2lem3  8642  cf0  8652  cfeq0  8657  cfsuc  8658  cflim2  8664  isfin5  8700  isfin4-3  8716  fin1a2lem11  8811  fin1a2lem12  8812  fin1a2lem13  8813  axcc2lem  8837  ac6num  8880  zornn0g  8906  ttukeylem3  8912  brdom3  8927  iundom2g  8936  cardeq0  8948  alephadd  8973  pwcfsdom  8979  axpowndlem3  8996  axpowndlem3OLD  8997  canthwe  9050  canthp1lem1  9051  pwxpndom2  9064  pwcdandom  9066  gchxpidm  9068  intwun  9134  0tsk  9154  grothomex  9228  indpi  9306  fzennn  12078  hash0  12437  hashen1  12439  hashmap  12493  hashbc  12502  hashf1  12506  hashge3el3dif  12524  swrdval  12644  swrd00  12645  swrd0  12658  cshfn  12761  cshnz  12763  0csh0  12764  incexclem  13648  incexc  13649  rexpen  13961  sadcf  14103  sadc0  14104  sadcp1  14105  smupf  14128  smup0  14129  smupp1  14130  0ram  14538  ram0  14540  cshws0  14586  str0  14670  ressbas  14687  ress0  14691  0rest  14827  xpscg  14955  xpscfn  14956  xpsc0  14957  xpsc1  14958  xpsfrnel  14960  xpsfrnel2  14962  xpsle  14978  ismred2  15000  acsfn  15056  0cat  15085  setcepi  15415  0pos  15584  meet0  15767  join0  15768  gsum0  15905  ga0  16336  psgn0fv0  16536  pmtrsn  16544  oppglsm  16662  efgi0  16738  vrgpf  16786  vrgpinv  16787  frgpuptinv  16789  frgpup2  16794  0frgp  16797  frgpnabllem1  16877  frgpnabllem2  16878  dprd0  17078  dmdprdpr  17098  dprdpr  17099  00lsp  17627  fvcoe1  18246  coe1f2  18248  coe1sfi  18252  coe1sfiOLD  18253  coe1add  18305  coe1mul2lem1  18308  coe1mul2lem2  18309  coe1mul2  18310  ply1coe  18337  ply1coeOLD  18338  evls1rhmlem  18358  evl1sca  18370  evl1var  18372  pf1mpf  18388  pf1ind  18391  frgpcyg  18612  frlmiscvec  18884  mat0dimscm  18971  mat0dimcrng  18972  mat0scmat  19040  mavmul0  19054  mavmul0g  19055  mvmumamul1  19056  mdet0pr  19094  mdet0f1o  19095  mdet0fv0  19096  mdetunilem9  19122  d0mat2pmat  19239  chpmat0d  19335  topgele  19435  en1top  19486  en2top  19487  sn0topon  19499  indistopon  19502  indistps  19512  indistps2  19513  sn0cld  19591  indiscld  19592  neipeltop  19630  rest0  19670  restsn  19671  cmpfi  19908  refun0  20016  txindislem  20134  hmphindis  20298  xpstopnlem1  20310  xpstopnlem2  20312  ptcmpfi  20314  snfil  20365  fbasfip  20369  fgcl  20379  filcon  20384  fbasrn  20385  cfinfil  20394  csdfil  20395  supfil  20396  ufildr  20432  fin1aufil  20433  rnelfmlem  20453  fclsval  20509  tmdgsum  20594  tsmsfbas  20626  ust0  20722  ustn0  20723  0met  20869  xpsdsval  20884  minveclem3b  21843  tdeglem2  22459  deg1ldg  22492  deg1leb  22495  deg1val  22496  deg1valOLD  22497  ulm0  22786  uhgra0  24309  uhgra0v  24310  umgra0  24325  usgra0  24370  usgra0v  24371  cusgra0v  24460  cusgra1v  24461  uvtx01vtx  24492  0wlk  24547  0trl  24548  0wlkon  24549  0trlon  24550  0pth  24572  0spth  24573  0pthon  24581  0pthonv  24583  0crct  24626  0cycl  24627  0conngra  24674  0clwlk  24765  vdgr0  24900  0egra0rgra  24936  0vgrargra  24937  frgra0v  24993  2spot0  25064  disjdifprg  27436  fpwrelmapffslem  27555  resvsca  27820  locfinref  27844  esumnul  28059  prsiga  28131  oms0  28266  eulerpartgbij  28311  eulerpartlemmf  28314  derang0  28613  indispcon  28679  rdgprc  29227  dfrdg3  29229  trpredpred  29311  trpred0  29319  nosgnn0  29418  nodense  29449  fullfunfnv  29596  fullfunfv  29597  rank0  29827  ssoninhaus  29913  onint1  29914  heibor1lem  30305  heiborlem6  30312  reheibor  30335  mzpcompact2lem  30684  wopprc  30972  pw2f1ocnv  30979  pwslnmlem0  31037  fnchoice  31404  0cnf  31679  dvnprodlem3  31745  afv0fv0  32234  ciclcl  32586  cicrcl  32587  cicer  32590  lincval0  33016  lco0  33028  linds0  33066  bnj941  33831  bnj97  33924  bnj149  33933  bnj150  33934  bnj944  33996  bj-1ex  34507  bj-0nel1  34509  bj-xpnzex  34516  bj-eltag  34535  bj-0eltag  34536  bj-tagss  34538  bj-pr1val  34562  bj-nuliota  34586  bj-nuliotaALT  34587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator