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

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

Proof of Theorem 0ex
StepHypRef Expression
1 ax-nul 4043 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3373 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1580 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 202 . 2  |-  E. x  x  =  (/)
54issetri 2732 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   _Vcvv 2725   (/)c0 3359
This theorem is referenced by:  class2set  4069  0elpw  4071  0nep0  4072  unidif0  4074  iin0  4075  notzfaus  4076  intv  4077  snexALT  4087  p0ex  4088  dtruALT  4098  zfpair  4103  snex  4107  dtruALT2  4110  opex  4127  opthwiener  4158  0elon  4335  nsuceq0  4362  snsn0non  4399  unisn2  4410  onint0  4475  tfinds2  4542  finds  4570  finds2  4572  opthprc  4640  xpexr  5018  soex  5026  dmsnsnsn  5054  nfunv  5140  fun0  5161  fvrn0  5400  fvssunirn  5401  brtpos0  6090  reldmtpos  6091  iotaex  6157  tfrlem16  6292  tz7.44-1  6302  seqomlem1  6345  1n0  6377  el1o  6381  om0  6399  map0e  6688  ixpexg  6723  0elixp  6730  en0  6806  ensn1  6807  en1  6810  2dom  6815  map1  6821  xp1en  6830  endisj  6831  pw2eng  6850  map2xp  6913  limensuci  6919  1sdom  6947  unxpdom2  6953  sucxpdom  6954  isinf  6958  ac6sfi  6983  fodomfi  7017  fi0  7054  oiexg  7131  brwdom  7162  brwdom2  7168  inf3lemb  7207  infeq5i  7218  dfom3  7229  cantnfvalf  7247  cantnfval2  7251  cantnflt  7254  cantnff  7256  cantnf0  7257  cantnfp1lem3  7263  cantnflem1d  7271  cantnflem1  7272  cantnf  7276  cnfcom  7284  tc0  7313  r10  7321  scottex  7436  infxpenlem  7522  fseqenlem1  7532  dfac9  7643  uncdadom  7678  cdaun  7679  cdaen  7680  cda1dif  7683  pm110.643  7684  cda0en  7686  cdacomen  7688  cdaassen  7689  xpcdaen  7690  mapcdaen  7691  cdaxpdom  7696  cdainf  7699  infcda1  7700  pwsdompw  7711  pwcdadom  7723  ackbij1lem14  7740  ackbij2lem2  7747  ackbij2lem3  7748  cf0  7758  cfeq0  7763  cfsuc  7764  cflim2  7770  isfin5  7806  isfin4-3  7822  fin1a2lem11  7917  fin1a2lem12  7918  fin1a2lem13  7919  axcc2lem  7943  ac6num  7987  zornn0g  8013  ttukeylem3  8019  brdom3  8034  iundom2g  8043  cardeq0  8053  alephadd  8076  pwcfsdom  8082  axpowndlem3  8098  canthwe  8150  canthp1lem1  8151  pwxpndom2  8164  pwcdandom  8166  gchxpidm  8168  intwun  8234  0tsk  8254  grothomex  8328  indpi  8408  fzennn  10873  hash0  11197  hashmap  11228  hashbc  11232  hashf1  11236  swrdval  11291  swrd00  11292  rexpen  12342  sadcf  12480  sadc0  12481  sadcp1  12482  smupf  12505  smup0  12506  smupp1  12507  0ram  12903  ram0  12905  str0  13020  ressbas  13034  ress0  13038  0rest  13170  xpscg  13296  xpscfn  13297  xpsc0  13298  xpsc1  13299  xpsfrnel  13301  xpsfrnel2  13303  xpsle  13319  ismred2  13339  acsfn  13367  0cat  13396  setcepi  13726  0pos  13894  meet0  14047  join0  14048  gsum0  14254  ga0  14549  oppglsm  14750  efgi0  14826  vrgpf  14874  vrgpinv  14875  frgpuptinv  14877  frgpup2  14882  0frgp  14885  frgpnabllem1  14958  frgpnabllem2  14959  dprd0  15063  dmdprdpr  15081  dprdpr  15082  00lsp  15535  fvcoe1  16082  coe1f2  16084  coe1sfi  16087  coe1add  16135  coe1mul2lem1  16138  coe1mul2lem2  16139  coe1mul2  16140  ply1coe  16162  frgpcyg  16321  topgele  16466  en1top  16516  en2top  16517  sn0topon  16529  indistopon  16532  indistps  16542  indistps2  16543  sn0cld  16621  indiscld  16622  rest0  16694  restsn  16695  cmpfi  16929  txindislem  17121  hmphindis  17282  xpstopnlem1  17294  xpstopnlem2  17296  ptcmpfi  17298  snfil  17353  fbasfip  17357  fgcl  17367  filcon  17372  fbasrn  17373  filuni  17374  cfinfil  17382  csdfil  17383  supfil  17384  ufildr  17420  fin1aufil  17421  rnelfmlem  17441  fclsval  17497  tmdgsum  17572  tsmsfbas  17604  0met  17724  xpsdsval  17739  minveclem3b  18586  evl1rhm  19206  evl1sca  19207  evl1var  19209  pf1mpf  19229  pf1ind  19232  tdeglem2  19241  deg1ldg  19272  deg1leb  19275  deg1val  19276  ulm0  19564  derang0  22800  indispcon  22865  umgra0  22977  vdgr0  22992  rdgprc  23248  dfrdg3  23250  trpredpred  23328  trpred0  23336  nosgnn0  23408  axdense  23440  fullfunfnv  23587  fullfunfv  23588  rank0  23903  ssoninhaus  23990  onint1  23991  alexeqd  24056  vxveqv  24148  ac5g  24169  snelpwg  24185  ab2rexexg  24217  fprg  24228  empos  24337  fisub  24649  0alg  24851  0ded  24852  0catOLD  24853  selsubf3g  25087  isconc1  25101  isconc2  25102  heibor1lem  25628  heiborlem6  25635  reheibor  25658  prter2  25844  mzpcompact2lem  25924  wopprc  26218  pw2f1ocnv  26225  pwslnmlem0  26288  bnj941  27431  bnj97  27525  bnj149  27534  bnj150  27535  bnj944  27597
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-nul 4043
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2727  df-dif 3078  df-nul 3360
  Copyright terms: Public domain W3C validator