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

Theorem 0ex 4448
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 4447. (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 4447 . . 3
2 eq0 3687 . . . 4
32exbii 1609 . . 3
41, 3mpbir 202 . 2
54issetri 3022 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  A.wal 1564  E.wex 1565  =wceq 1670  e.wcel 1732   cvv 3015   c0 3673
This theorem is referenced by:  sseliALT  4449  csbexg  4450  unisn2  4454  class2set  4482  0elpw  4484  0nep0  4486  unidif0  4488  iin0  4489  notzfaus  4490  intv  4491  snexALT  4501  p0ex  4502  dtruALT  4547  zfpair  4552  snex  4556  dtruALT2  4559  opex  4579  opthwiener  4615  0elon  4793  nsuceq0  4820  snsn0non  4859  opthprc  4908  dmsnsnsn  5337  iotaex  5418  nfunv  5469  fun0  5493  fvrn0  5729  fvssunirn  5730  fprg  5906  onint0  6417  tfinds2  6484  finds  6512  finds2  6514  xpexr  6527  soex  6529  brtpos0  6718  reldmtpos  6719  tfrlem16  6816  tz7.44-1  6826  seqomlem1  6869  1n0  6901  el1o  6905  om0  6923  map0e  7214  ixpexg  7250  0elixp  7257  en0  7334  ensn1  7335  en1  7338  2dom  7344  map1  7350  xp1en  7359  endisj  7360  pw2eng  7379  map2xp  7442  limensuci  7448  1sdom  7476  unxpdom2  7482  sucxpdom  7483  isinf  7487  ac6sfi  7517  fodomfi  7551  fi0  7592  oiexg  7671  brwdom  7702  brwdom2  7708  inf3lemb  7747  infeq5i  7758  dfom3  7769  cantnfvalf  7787  cantnfval2  7791  cantnflt  7794  cantnff  7796  cantnf0  7797  cantnfp1lem3  7803  cantnflem1d  7811  cantnflem1  7812  cantnf  7816  cnfcom  7824  tc0  7853  r10  7861  scottex  7978  infxpenlem  8066  fseqenlem1  8076  uncdadom  8222  cdaun  8223  cdaen  8224  cda1dif  8227  pm110.643  8228  cda0en  8230  cdacomen  8232  cdaassen  8233  xpcdaen  8234  mapcdaen  8235  cdaxpdom  8240  cdainf  8243  infcda1  8244  pwsdompw  8255  pwcdadom  8267  ackbij1lem14  8284  ackbij2lem2  8291  ackbij2lem3  8292  cf0  8302  cfeq0  8307  cfsuc  8308  cflim2  8314  isfin5  8350  isfin4-3  8366  fin1a2lem11  8461  fin1a2lem12  8462  fin1a2lem13  8463  axcc2lem  8487  ac6num  8530  zornn0g  8556  ttukeylem3  8562  brdom3  8577  iundom2g  8586  cardeq0  8598  alephadd  8623  pwcfsdom  8629  axpowndlem3  8645  canthwe  8697  canthp1lem1  8698  pwxpndom2  8711  pwcdandom  8713  gchxpidm  8715  intwun  8781  0tsk  8801  grothomex  8875  indpi  8955  fzennn  11639  hash0  11984  hashmap  12044  hashbc  12053  hashf1  12057  swrdval  12160  swrd00  12161  swrd0  12174  cshfn  12274  cshnz  12276  0csh0  12277  incexclem  13146  incexc  13147  rexpen  13357  sadcf  13496  sadc0  13497  sadcp1  13498  smupf  13521  smup0  13522  smupp1  13523  0ram  13928  ram0  13930  cshws0  13975  str0  14059  ressbas  14073  ress0  14077  0rest  14211  xpscg  14337  xpscfn  14338  xpsc0  14339  xpsc1  14340  xpsfrnel  14342  xpsfrnel2  14344  xpsle  14360  ismred2  14382  acsfn  14438  0cat  14467  setcepi  14797  0pos  14965  meet0  15148  join0  15149  gsum0  15348  ga0  15646  oppglsm  15885  efgi0  15961  vrgpf  16009  vrgpinv  16010  frgpuptinv  16012  frgpup2  16017  0frgp  16020  frgpnabllem1  16094  frgpnabllem2  16095  dprd0  16204  dmdprdpr  16222  dprdpr  16223  00lsp  16676  fvcoe1  17230  coe1f2  17232  coe1sfi  17235  coe1add  17282  coe1mul2lem1  17285  coe1mul2lem2  17286  coe1mul2  17287  ply1coe  17309  frgpcyg  17479  psgn0fv0  17664  mavmul0  17833  mavmul0g  17834  mdet0pr  17875  mdet0f1o  17876  mdet0fv0  17877  mdetunilem9  17898  topgele  18013  en1top  18063  en2top  18064  sn0topon  18076  indistopon  18079  indistps  18089  indistps2  18090  sn0cld  18168  indiscld  18169  neipeltop  18207  rest0  18247  restsn  18248  cmpfi  18485  txindislem  18680  hmphindis  18844  xpstopnlem1  18856  xpstopnlem2  18858  ptcmpfi  18860  snfil  18911  fbasfip  18915  fgcl  18925  filcon  18930  fbasrn  18931  cfinfil  18940  csdfil  18941  supfil  18942  ufildr  18978  fin1aufil  18979  rnelfmlem  18999  fclsval  19055  tmdgsum  19140  tsmsfbas  19172  ust0  19264  ustn0  19265  0met  19411  xpsdsval  19426  minveclem3b  20344  evl1rhm  20964  evl1sca  20965  evl1var  20967  pf1mpf  20987  pf1ind  20990  tdeglem2  20999  deg1ldg  21030  deg1leb  21033  deg1val  21034  ulm0  21322  uhgra0  22365  uhgra0v  22366  umgra0  22381  usgra0  22411  usgra0v  22412  cusgra0v  22490  cusgra1v  22491  uvtx01vtx  22522  0wlk  22566  0trl  22567  0wlkon  22568  0trlon  22569  0pth  22591  0spth  22592  0pthon  22600  0pthonv  22602  0crct  22634  0cycl  22635  0conngra  22682  vdgr0  22692  disjdifprg  25047  resvsca  25466  esumnul  25682  prsiga  25754  derang0  26203  indispcon  26269  rdgprc  26761  dfrdg3  26763  trpredpred  26845  trpred0  26853  nosgnn0  26952  nodense  26983  fullfunfnv  27130  fullfunfv  27131  rank0  27450  ssoninhaus  27537  onint1  27538  heibor1lem  27890  heiborlem6  27897  reheibor  27920  mzpcompact2lem  28236  wopprc  28527  pw2f1ocnv  28534  pwslnmlem0  28592  fnchoice  28926  afv0fv0  29234  0clwlk  29609  0egra0rgra  29730  0vgrargra  29731  frgra0v  29766  2spot0  29838  bnj941  30613  bnj97  30707  bnj149  30716  bnj150  30717  bnj944  30779  bj-eltag  30959  bj-tagss  30960  bj-xpnzex  30970  bj-pr1val  30980  bj-2upleex  30985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-nul 4447
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-v 3017  df-dif 3368  df-nul 3674
  Copyright terms: Public domain W3C validator