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

Theorem 0ex 4373
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 4372. (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 4372 . . 3
2 eq0 3630 . . . 4
32exbii 1593 . . 3
41, 3mpbir 202 . 2
54issetri 2972 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  A.wal 1550  E.wex 1551  =wceq 1654  e.wcel 1728   cvv 2965   c0 3616
This theorem is referenced by:  sseliALT  4374  csbexg  4375  class2set  4406  0elpw  4408  0nep0  4409  unidif0  4411  iin0  4412  notzfaus  4413  intv  4414  snexALT  4424  p0ex  4425  dtruALT  4435  zfpair  4440  snex  4444  dtruALT2  4447  opex  4466  opthwiener  4497  0elon  4675  nsuceq0  4702  snsn0non  4741  unisn2  4752  onint0  4817  tfinds2  4884  finds  4912  finds2  4914  opthprc  4965  xpexr  5351  soex  5363  dmsnsnsn  5394  iotaex  5481  nfunv  5531  fun0  5555  fvrn0  5796  fvssunirn  5797  fprg  5963  brtpos0  6536  reldmtpos  6537  tfrlem16  6703  tz7.44-1  6713  seqomlem1  6756  1n0  6788  el1o  6792  om0  6810  map0e  7100  ixpexg  7135  0elixp  7142  en0  7219  ensn1  7220  en1  7223  2dom  7228  map1  7234  xp1en  7243  endisj  7244  pw2eng  7263  map2xp  7326  limensuci  7332  1sdom  7360  unxpdom2  7366  sucxpdom  7367  isinf  7371  ac6sfi  7400  fodomfi  7434  fi0  7474  oiexg  7553  brwdom  7584  brwdom2  7590  inf3lemb  7629  infeq5i  7640  dfom3  7651  cantnfvalf  7669  cantnfval2  7673  cantnflt  7676  cantnff  7678  cantnf0  7679  cantnfp1lem3  7685  cantnflem1d  7693  cantnflem1  7694  cantnf  7698  cnfcom  7706  tc0  7735  r10  7743  scottex  7860  infxpenlem  7946  fseqenlem1  7956  uncdadom  8102  cdaun  8103  cdaen  8104  cda1dif  8107  pm110.643  8108  cda0en  8110  cdacomen  8112  cdaassen  8113  xpcdaen  8114  mapcdaen  8115  cdaxpdom  8120  cdainf  8123  infcda1  8124  pwsdompw  8135  pwcdadom  8147  ackbij1lem14  8164  ackbij2lem2  8171  ackbij2lem3  8172  cf0  8182  cfeq0  8187  cfsuc  8188  cflim2  8194  isfin5  8230  isfin4-3  8246  fin1a2lem11  8341  fin1a2lem12  8342  fin1a2lem13  8343  axcc2lem  8367  ac6num  8410  zornn0g  8436  ttukeylem3  8442  brdom3  8457  iundom2g  8466  cardeq0  8478  alephadd  8503  pwcfsdom  8509  axpowndlem3  8525  canthwe  8577  canthp1lem1  8578  pwxpndom2  8591  pwcdandom  8593  gchxpidm  8595  intwun  8661  0tsk  8681  grothomex  8755  indpi  8835  fzennn  11358  hash0  11697  hashmap  11749  hashbc  11753  hashf1  11757  swrdval  11815  swrd00  11816  incexclem  12667  incexc  12668  rexpen  12878  sadcf  13016  sadc0  13017  sadcp1  13018  smupf  13041  smup0  13042  smupp1  13043  0ram  13439  ram0  13441  str0  13556  ressbas  13570  ress0  13574  0rest  13708  xpscg  13834  xpscfn  13835  xpsc0  13836  xpsc1  13837  xpsfrnel  13839  xpsfrnel2  13841  xpsle  13857  ismred2  13879  acsfn  13935  0cat  13964  setcepi  14294  0pos  14462  meet0  14615  join0  14616  gsum0  14831  ga0  15126  oppglsm  15327  efgi0  15403  vrgpf  15451  vrgpinv  15452  frgpuptinv  15454  frgpup2  15459  0frgp  15462  frgpnabllem1  15535  frgpnabllem2  15536  dprd0  15640  dmdprdpr  15658  dprdpr  15659  00lsp  16108  fvcoe1  16656  coe1f2  16658  coe1sfi  16661  coe1add  16708  coe1mul2lem1  16711  coe1mul2lem2  16712  coe1mul2  16713  ply1coe  16735  frgpcyg  16905  topgele  17050  en1top  17100  en2top  17101  sn0topon  17113  indistopon  17116  indistps  17126  indistps2  17127  sn0cld  17205  indiscld  17206  neipeltop  17244  rest0  17284  restsn  17285  cmpfi  17522  txindislem  17716  hmphindis  17880  xpstopnlem1  17892  xpstopnlem2  17894  ptcmpfi  17896  snfil  17947  fbasfip  17951  fgcl  17961  filcon  17966  fbasrn  17967  cfinfil  17976  csdfil  17977  supfil  17978  ufildr  18014  fin1aufil  18015  rnelfmlem  18035  fclsval  18091  tmdgsum  18176  tsmsfbas  18208  ust0  18300  ustn0  18301  0met  18447  xpsdsval  18462  minveclem3b  19380  evl1rhm  20000  evl1sca  20001  evl1var  20003  pf1mpf  20023  pf1ind  20026  tdeglem2  20035  deg1ldg  20066  deg1leb  20069  deg1val  20070  ulm0  20358  uhgra0  21395  uhgra0v  21396  umgra0  21411  usgra0  21441  usgra0v  21442  cusgra0v  21520  cusgra1v  21521  uvtx01vtx  21552  0wlk  21596  0trl  21597  0wlkon  21598  0trlon  21599  0pth  21621  0spth  21622  0pthon  21630  0pthonv  21632  0crct  21664  0cycl  21665  0conngra  21712  vdgr0  21722  disjdifprg  24066  esumnul  24492  prsiga  24563  derang0  24959  indispcon  25025  rdgprc  25526  dfrdg3  25528  trpredpred  25610  trpred0  25618  nosgnn0  25717  nodense  25748  fullfunfnv  25895  fullfunfv  25896  rank0  26215  ssoninhaus  26302  onint1  26303  heibor1lem  26629  heiborlem6  26636  reheibor  26659  mzpcompact2lem  26989  wopprc  27280  pw2f1ocnv  27287  pwslnmlem0  27349  fnchoice  27854  afv0fv0  28168  swrd0  28381  0egra0rgra  28611  0vgrargra  28612  frgra0v  28621  2spot0  28691  bnj941  29384  bnj97  29478  bnj149  29487  bnj150  29488  bnj944  29550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-nul 4372
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2967  df-dif 3312  df-nul 3617
  Copyright terms: Public domain W3C validator