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

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

Proof of Theorem 0ex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 4369 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3630 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1593 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 202 . 2  |-  E. x  x  =  (/)
54issetri 2972 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1550   E.wex 1551    = wceq 1654    e. wcel 1728   _Vcvv 2965   (/)c0 3616
This theorem is referenced by:  csbexg  4371  class2set  4402  0elpw  4404  0nep0  4405  unidif0  4407  iin0  4408  notzfaus  4409  intv  4410  snexALT  4420  p0ex  4421  dtruALT  4431  zfpair  4436  snex  4440  dtruALT2  4443  opex  4462  opthwiener  4493  0elon  4669  nsuceq0  4696  snsn0non  4735  unisn2  4746  onint0  4811  tfinds2  4878  finds  4906  finds2  4908  opthprc  4960  xpexr  5342  soex  5354  dmsnsnsn  5383  iotaex  5470  nfunv  5519  fun0  5543  fvrn0  5784  fvssunirn  5785  fprg  5951  brtpos0  6522  reldmtpos  6523  tfrlem16  6690  tz7.44-1  6700  seqomlem1  6743  1n0  6775  el1o  6779  om0  6797  map0e  7087  ixpexg  7122  0elixp  7129  en0  7206  ensn1  7207  en1  7210  2dom  7215  map1  7221  xp1en  7230  endisj  7231  pw2eng  7250  map2xp  7313  limensuci  7319  1sdom  7347  unxpdom2  7353  sucxpdom  7354  isinf  7358  ac6sfi  7387  fodomfi  7421  fi0  7461  oiexg  7540  brwdom  7571  brwdom2  7577  inf3lemb  7616  infeq5i  7627  dfom3  7638  cantnfvalf  7656  cantnfval2  7660  cantnflt  7663  cantnff  7665  cantnf0  7666  cantnfp1lem3  7672  cantnflem1d  7680  cantnflem1  7681  cantnf  7685  cnfcom  7693  tc0  7722  r10  7730  scottex  7847  infxpenlem  7933  fseqenlem1  7943  uncdadom  8089  cdaun  8090  cdaen  8091  cda1dif  8094  pm110.643  8095  cda0en  8097  cdacomen  8099  cdaassen  8100  xpcdaen  8101  mapcdaen  8102  cdaxpdom  8107  cdainf  8110  infcda1  8111  pwsdompw  8122  pwcdadom  8134  ackbij1lem14  8151  ackbij2lem2  8158  ackbij2lem3  8159  cf0  8169  cfeq0  8174  cfsuc  8175  cflim2  8181  isfin5  8217  isfin4-3  8233  fin1a2lem11  8328  fin1a2lem12  8329  fin1a2lem13  8330  axcc2lem  8354  ac6num  8397  zornn0g  8423  ttukeylem3  8429  brdom3  8444  iundom2g  8453  cardeq0  8465  alephadd  8490  pwcfsdom  8496  axpowndlem3  8512  canthwe  8564  canthp1lem1  8565  pwxpndom2  8578  pwcdandom  8580  gchxpidm  8582  intwun  8648  0tsk  8668  grothomex  8742  indpi  8822  fzennn  11345  hash0  11684  hashmap  11736  hashbc  11740  hashf1  11744  swrdval  11802  swrd00  11803  incexclem  12654  incexc  12655  rexpen  12865  sadcf  13003  sadc0  13004  sadcp1  13005  smupf  13028  smup0  13029  smupp1  13030  0ram  13426  ram0  13428  str0  13543  ressbas  13557  ress0  13561  0rest  13695  xpscg  13821  xpscfn  13822  xpsc0  13823  xpsc1  13824  xpsfrnel  13826  xpsfrnel2  13828  xpsle  13844  ismred2  13866  acsfn  13922  0cat  13951  setcepi  14281  0pos  14449  meet0  14602  join0  14603  gsum0  14818  ga0  15113  oppglsm  15314  efgi0  15390  vrgpf  15438  vrgpinv  15439  frgpuptinv  15441  frgpup2  15446  0frgp  15449  frgpnabllem1  15522  frgpnabllem2  15523  dprd0  15627  dmdprdpr  15645  dprdpr  15646  00lsp  16095  fvcoe1  16643  coe1f2  16645  coe1sfi  16648  coe1add  16695  coe1mul2lem1  16698  coe1mul2lem2  16699  coe1mul2  16700  ply1coe  16722  frgpcyg  16892  topgele  17037  en1top  17087  en2top  17088  sn0topon  17100  indistopon  17103  indistps  17113  indistps2  17114  sn0cld  17192  indiscld  17193  neipeltop  17231  rest0  17271  restsn  17272  cmpfi  17509  txindislem  17703  hmphindis  17867  xpstopnlem1  17879  xpstopnlem2  17881  ptcmpfi  17883  snfil  17934  fbasfip  17938  fgcl  17948  filcon  17953  fbasrn  17954  filuni  17955  cfinfil  17963  csdfil  17964  supfil  17965  ufildr  18001  fin1aufil  18002  rnelfmlem  18022  fclsval  18078  tmdgsum  18163  tsmsfbas  18195  ust0  18287  ustn0  18288  0met  18434  xpsdsval  18449  minveclem3b  19367  evl1rhm  19987  evl1sca  19988  evl1var  19990  pf1mpf  20010  pf1ind  20013  tdeglem2  20022  deg1ldg  20053  deg1leb  20056  deg1val  20057  ulm0  20345  uhgra0  21382  uhgra0v  21383  umgra0  21398  usgra0  21428  usgra0v  21429  cusgra0v  21507  cusgra1v  21508  uvtx01vtx  21539  0wlk  21583  0trl  21584  0wlkon  21585  0trlon  21586  0pth  21608  0spth  21609  0pthon  21617  0pthonv  21619  0crct  21651  0cycl  21652  0conngra  21699  vdgr0  21709  disjdifprg  24052  esumnul  24478  prsiga  24549  derang0  24890  indispcon  24956  rdgprc  25457  dfrdg3  25459  trpredpred  25541  trpred0  25549  nosgnn0  25648  nodense  25679  fullfunfnv  25826  fullfunfv  25827  rank0  26146  ssoninhaus  26233  onint1  26234  heibor1lem  26560  heiborlem6  26567  reheibor  26590  mzpcompact2lem  26920  wopprc  27213  pw2f1ocnv  27220  pwslnmlem0  27282  fnchoice  27788  afv0fv0  28101  swrd0  28315  0egra0rgra  28545  0vgrargra  28546  frgra0v  28555  2spot0  28625  bnj941  29317  bnj97  29411  bnj149  29420  bnj150  29421  bnj944  29483
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 4369
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