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

Theorem 0ex 4151
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 4150. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex  |-  (/)  e.  _V
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem 0ex
StepHypRef Expression
1 ax-nul 4150 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3470 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1570 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 202 . 2  |-  E. x  x  =  (/)
54issetri 2796 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5   A.wal 1528   E.wex 1529    = wceq 1624    e. wcel 1685   _Vcvv 2789   (/)c0 3456
This theorem is referenced by:  class2set  4177  0elpw  4179  0nep0  4180  unidif0  4182  iin0  4183  notzfaus  4184  intv  4185  snexALT  4195  p0ex  4196  dtruALT  4206  zfpair  4211  snex  4215  dtruALT2  4218  opex  4236  opthwiener  4267  0elon  4444  nsuceq0  4471  snsn0non  4510  unisn2  4521  onint0  4586  tfinds2  4653  finds  4681  finds2  4683  opthprc  4735  xpexr  5113  soex  5121  dmsnsnsn  5149  nfunv  5251  fun0  5272  fvrn0  5511  fvssunirn  5512  brtpos0  6202  reldmtpos  6203  iotaex  6269  tfrlem16  6404  tz7.44-1  6414  seqomlem1  6457  1n0  6489  el1o  6493  om0  6511  map0e  6800  ixpexg  6835  0elixp  6842  en0  6919  ensn1  6920  en1  6923  2dom  6928  map1  6934  xp1en  6943  endisj  6944  pw2eng  6963  map2xp  7026  limensuci  7032  1sdom  7060  unxpdom2  7066  sucxpdom  7067  isinf  7071  ac6sfi  7096  fodomfi  7130  fi0  7168  oiexg  7245  brwdom  7276  brwdom2  7282  inf3lemb  7321  infeq5i  7332  dfom3  7343  cantnfvalf  7361  cantnfval2  7365  cantnflt  7368  cantnff  7370  cantnf0  7371  cantnfp1lem3  7377  cantnflem1d  7385  cantnflem1  7386  cantnf  7390  cnfcom  7398  tc0  7427  r10  7435  scottex  7550  infxpenlem  7636  fseqenlem1  7646  dfac9  7757  uncdadom  7792  cdaun  7793  cdaen  7794  cda1dif  7797  pm110.643  7798  cda0en  7800  cdacomen  7802  cdaassen  7803  xpcdaen  7804  mapcdaen  7805  cdaxpdom  7810  cdainf  7813  infcda1  7814  pwsdompw  7825  pwcdadom  7837  ackbij1lem14  7854  ackbij2lem2  7861  ackbij2lem3  7862  cf0  7872  cfeq0  7877  cfsuc  7878  cflim2  7884  isfin5  7920  isfin4-3  7936  fin1a2lem11  8031  fin1a2lem12  8032  fin1a2lem13  8033  axcc2lem  8057  ac6num  8101  zornn0g  8127  ttukeylem3  8133  brdom3  8148  iundom2g  8157  cardeq0  8169  alephadd  8194  pwcfsdom  8200  axpowndlem3  8216  canthwe  8268  canthp1lem1  8269  pwxpndom2  8282  pwcdandom  8284  gchxpidm  8286  intwun  8352  0tsk  8372  grothomex  8446  indpi  8526  fzennn  11024  hash0  11349  hashmap  11381  hashbc  11385  hashf1  11389  swrdval  11444  swrd00  11445  incexclem  12289  incexc  12290  rexpen  12500  sadcf  12638  sadc0  12639  sadcp1  12640  smupf  12663  smup0  12664  smupp1  12665  0ram  13061  ram0  13063  str0  13178  ressbas  13192  ress0  13196  0rest  13328  xpscg  13454  xpscfn  13455  xpsc0  13456  xpsc1  13457  xpsfrnel  13459  xpsfrnel2  13461  xpsle  13477  ismred2  13499  acsfn  13555  0cat  13584  setcepi  13914  0pos  14082  meet0  14235  join0  14236  gsum0  14451  ga0  14746  oppglsm  14947  efgi0  15023  vrgpf  15071  vrgpinv  15072  frgpuptinv  15074  frgpup2  15079  0frgp  15082  frgpnabllem1  15155  frgpnabllem2  15156  dprd0  15260  dmdprdpr  15278  dprdpr  15279  00lsp  15732  fvcoe1  16282  coe1f2  16284  coe1sfi  16287  coe1add  16335  coe1mul2lem1  16338  coe1mul2lem2  16339  coe1mul2  16340  ply1coe  16362  frgpcyg  16521  topgele  16666  en1top  16716  en2top  16717  sn0topon  16729  indistopon  16732  indistps  16742  indistps2  16743  sn0cld  16821  indiscld  16822  rest0  16894  restsn  16895  cmpfi  17129  txindislem  17321  hmphindis  17482  xpstopnlem1  17494  xpstopnlem2  17496  ptcmpfi  17498  snfil  17553  fbasfip  17557  fgcl  17567  filcon  17572  fbasrn  17573  filuni  17574  cfinfil  17582  csdfil  17583  supfil  17584  ufildr  17620  fin1aufil  17621  rnelfmlem  17641  fclsval  17697  tmdgsum  17772  tsmsfbas  17804  0met  17924  xpsdsval  17939  minveclem3b  18786  evl1rhm  19406  evl1sca  19407  evl1var  19409  pf1mpf  19429  pf1ind  19432  tdeglem2  19441  deg1ldg  19472  deg1leb  19475  deg1val  19476  ulm0  19764  derang0  23104  indispcon  23169  umgra0  23281  vdgr0  23296  rdgprc  23552  dfrdg3  23554  trpredpred  23632  trpred0  23640  nosgnn0  23712  axdense  23744  fullfunfnv  23891  fullfunfv  23892  rank0  24207  ssoninhaus  24294  onint1  24295  alexeqd  24360  vxveqv  24452  ac5g  24473  snelpwg  24489  ab2rexexg  24521  fprg  24532  empos  24641  fisub  24953  0alg  25155  0ded  25156  0catOLD  25157  selsubf3g  25391  isconc1  25405  isconc2  25406  heibor1lem  25932  heiborlem6  25939  reheibor  25962  prter2  26148  mzpcompact2lem  26228  wopprc  26522  pw2f1ocnv  26529  pwslnmlem0  26592  fnchoice  27099  afv0fv0  27389  bnj941  28071  bnj97  28165  bnj149  28174  bnj150  28175  bnj944  28237
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-nul 4150
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator