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

Theorem 0ex 4047
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 4046. (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 4046 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3376 . . . 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 2734 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 2727   (/)c0 3362
This theorem is referenced by:  class2set  4072  0elpw  4074  0nep0  4075  unidif0  4077  iin0  4078  notzfaus  4079  intv  4080  snexALT  4090  p0ex  4091  dtruALT  4101  zfpair  4106  snex  4110  dtruALT2  4113  opex  4130  opthwiener  4161  0elon  4338  nsuceq0  4365  snsn0non  4402  unisn2  4413  onint0  4478  tfinds2  4545  finds  4573  finds2  4575  opthprc  4643  xpexr  5021  soex  5029  dmsnsnsn  5057  nfunv  5143  fun0  5164  fvrn0  5403  fvssunirn  5404  brtpos0  6093  reldmtpos  6094  iotaex  6160  tfrlem16  6295  tz7.44-1  6305  seqomlem1  6348  1n0  6380  el1o  6384  om0  6402  map0e  6691  ixpexg  6726  0elixp  6733  en0  6809  ensn1  6810  en1  6813  2dom  6818  map1  6824  xp1en  6833  endisj  6834  pw2eng  6853  map2xp  6916  limensuci  6922  1sdom  6950  unxpdom2  6956  sucxpdom  6957  isinf  6961  ac6sfi  6986  fodomfi  7020  fi0  7057  oiexg  7134  brwdom  7165  brwdom2  7171  inf3lemb  7210  infeq5i  7221  dfom3  7232  cantnfvalf  7250  cantnfval2  7254  cantnflt  7257  cantnff  7259  cantnf0  7260  cantnfp1lem3  7266  cantnflem1d  7274  cantnflem1  7275  cantnf  7279  cnfcom  7287  tc0  7316  r10  7324  scottex  7439  infxpenlem  7525  fseqenlem1  7535  dfac9  7646  uncdadom  7681  cdaun  7682  cdaen  7683  cda1dif  7686  pm110.643  7687  cda0en  7689  cdacomen  7691  cdaassen  7692  xpcdaen  7693  mapcdaen  7694  cdaxpdom  7699  cdainf  7702  infcda1  7703  pwsdompw  7714  pwcdadom  7726  ackbij1lem14  7743  ackbij2lem2  7750  ackbij2lem3  7751  cf0  7761  cfeq0  7766  cfsuc  7767  cflim2  7773  isfin5  7809  isfin4-3  7825  fin1a2lem11  7920  fin1a2lem12  7921  fin1a2lem13  7922  axcc2lem  7946  ac6num  7990  zornn0g  8016  ttukeylem3  8022  brdom3  8037  iundom2g  8046  cardeq0  8056  alephadd  8079  pwcfsdom  8085  axpowndlem3  8101  canthwe  8153  canthp1lem1  8154  pwxpndom2  8167  pwcdandom  8169  gchxpidm  8171  intwun  8237  0tsk  8257  grothomex  8331  indpi  8411  fzennn  10908  hash0  11233  hashmap  11264  hashbc  11268  hashf1  11272  swrdval  11327  swrd00  11328  rexpen  12380  sadcf  12518  sadc0  12519  sadcp1  12520  smupf  12543  smup0  12544  smupp1  12545  0ram  12941  ram0  12943  str0  13058  ressbas  13072  ress0  13076  0rest  13208  xpscg  13334  xpscfn  13335  xpsc0  13336  xpsc1  13337  xpsfrnel  13339  xpsfrnel2  13341  xpsle  13357  ismred2  13377  acsfn  13405  0cat  13434  setcepi  13764  0pos  13932  meet0  14085  join0  14086  gsum0  14292  ga0  14587  oppglsm  14788  efgi0  14864  vrgpf  14912  vrgpinv  14913  frgpuptinv  14915  frgpup2  14920  0frgp  14923  frgpnabllem1  14996  frgpnabllem2  14997  dprd0  15101  dmdprdpr  15119  dprdpr  15120  00lsp  15573  fvcoe1  16120  coe1f2  16122  coe1sfi  16125  coe1add  16173  coe1mul2lem1  16176  coe1mul2lem2  16177  coe1mul2  16178  ply1coe  16200  frgpcyg  16359  topgele  16504  en1top  16554  en2top  16555  sn0topon  16567  indistopon  16570  indistps  16580  indistps2  16581  sn0cld  16659  indiscld  16660  rest0  16732  restsn  16733  cmpfi  16967  txindislem  17159  hmphindis  17320  xpstopnlem1  17332  xpstopnlem2  17334  ptcmpfi  17336  snfil  17391  fbasfip  17395  fgcl  17405  filcon  17410  fbasrn  17411  filuni  17412  cfinfil  17420  csdfil  17421  supfil  17422  ufildr  17458  fin1aufil  17459  rnelfmlem  17479  fclsval  17535  tmdgsum  17610  tsmsfbas  17642  0met  17762  xpsdsval  17777  minveclem3b  18624  evl1rhm  19244  evl1sca  19245  evl1var  19247  pf1mpf  19267  pf1ind  19270  tdeglem2  19279  deg1ldg  19310  deg1leb  19313  deg1val  19314  ulm0  19602  derang0  22871  indispcon  22936  umgra0  23048  vdgr0  23063  rdgprc  23319  dfrdg3  23321  trpredpred  23399  trpred0  23407  nosgnn0  23479  axdense  23511  fullfunfnv  23658  fullfunfv  23659  rank0  23974  ssoninhaus  24061  onint1  24062  alexeqd  24127  vxveqv  24219  ac5g  24240  snelpwg  24256  ab2rexexg  24288  fprg  24299  empos  24408  fisub  24720  0alg  24922  0ded  24923  0catOLD  24924  selsubf3g  25158  isconc1  25172  isconc2  25173  heibor1lem  25699  heiborlem6  25706  reheibor  25729  prter2  25915  mzpcompact2lem  25995  wopprc  26289  pw2f1ocnv  26296  pwslnmlem0  26359  bnj941  27493  bnj97  27587  bnj149  27596  bnj150  27597  bnj944  27659
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 4046
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 2729  df-dif 3081  df-nul 3363
  Copyright terms: Public domain W3C validator