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

Theorem 0ex 4331
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 4330. (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 4330 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3634 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1592 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 201 . 2  |-  E. x  x  =  (/)
54issetri 2955 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948   (/)c0 3620
This theorem is referenced by:  class2set  4359  0elpw  4361  0nep0  4362  unidif0  4364  iin0  4365  notzfaus  4366  intv  4367  snexALT  4377  p0ex  4378  dtruALT  4388  zfpair  4393  snex  4397  dtruALT2  4400  opex  4419  opthwiener  4450  0elon  4626  nsuceq0  4653  snsn0non  4691  unisn2  4702  onint0  4767  tfinds2  4834  finds  4862  finds2  4864  opthprc  4916  xpexr  5298  soex  5310  dmsnsnsn  5339  iotaex  5426  nfunv  5475  fun0  5499  fvrn0  5744  fvssunirn  5745  fprg  5906  brtpos0  6477  reldmtpos  6478  tfrlem16  6645  tz7.44-1  6655  seqomlem1  6698  1n0  6730  el1o  6734  om0  6752  map0e  7042  ixpexg  7077  0elixp  7084  en0  7161  ensn1  7162  en1  7165  2dom  7170  map1  7176  xp1en  7185  endisj  7186  pw2eng  7205  map2xp  7268  limensuci  7274  1sdom  7302  unxpdom2  7308  sucxpdom  7309  isinf  7313  ac6sfi  7342  fodomfi  7376  fi0  7416  oiexg  7493  brwdom  7524  brwdom2  7530  inf3lemb  7569  infeq5i  7580  dfom3  7591  cantnfvalf  7609  cantnfval2  7613  cantnflt  7616  cantnff  7618  cantnf0  7619  cantnfp1lem3  7625  cantnflem1d  7633  cantnflem1  7634  cantnf  7638  cnfcom  7646  tc0  7675  r10  7683  scottex  7798  infxpenlem  7884  fseqenlem1  7894  uncdadom  8040  cdaun  8041  cdaen  8042  cda1dif  8045  pm110.643  8046  cda0en  8048  cdacomen  8050  cdaassen  8051  xpcdaen  8052  mapcdaen  8053  cdaxpdom  8058  cdainf  8061  infcda1  8062  pwsdompw  8073  pwcdadom  8085  ackbij1lem14  8102  ackbij2lem2  8109  ackbij2lem3  8110  cf0  8120  cfeq0  8125  cfsuc  8126  cflim2  8132  isfin5  8168  isfin4-3  8184  fin1a2lem11  8279  fin1a2lem12  8280  fin1a2lem13  8281  axcc2lem  8305  ac6num  8348  zornn0g  8374  ttukeylem3  8380  brdom3  8395  iundom2g  8404  cardeq0  8416  alephadd  8441  pwcfsdom  8447  axpowndlem3  8463  canthwe  8515  canthp1lem1  8516  pwxpndom2  8529  pwcdandom  8531  gchxpidm  8533  intwun  8599  0tsk  8619  grothomex  8693  indpi  8773  fzennn  11295  hash0  11634  hashmap  11686  hashbc  11690  hashf1  11694  swrdval  11752  swrd00  11753  incexclem  12604  incexc  12605  rexpen  12815  sadcf  12953  sadc0  12954  sadcp1  12955  smupf  12978  smup0  12979  smupp1  12980  0ram  13376  ram0  13378  str0  13493  ressbas  13507  ress0  13511  0rest  13645  xpscg  13771  xpscfn  13772  xpsc0  13773  xpsc1  13774  xpsfrnel  13776  xpsfrnel2  13778  xpsle  13794  ismred2  13816  acsfn  13872  0cat  13901  setcepi  14231  0pos  14399  meet0  14552  join0  14553  gsum0  14768  ga0  15063  oppglsm  15264  efgi0  15340  vrgpf  15388  vrgpinv  15389  frgpuptinv  15391  frgpup2  15396  0frgp  15399  frgpnabllem1  15472  frgpnabllem2  15473  dprd0  15577  dmdprdpr  15595  dprdpr  15596  00lsp  16045  fvcoe1  16593  coe1f2  16595  coe1sfi  16598  coe1add  16645  coe1mul2lem1  16648  coe1mul2lem2  16649  coe1mul2  16650  ply1coe  16672  frgpcyg  16842  topgele  16987  en1top  17037  en2top  17038  sn0topon  17050  indistopon  17053  indistps  17063  indistps2  17064  sn0cld  17142  indiscld  17143  neipeltop  17181  rest0  17221  restsn  17222  cmpfi  17459  txindislem  17653  hmphindis  17817  xpstopnlem1  17829  xpstopnlem2  17831  ptcmpfi  17833  snfil  17884  fbasfip  17888  fgcl  17898  filcon  17903  fbasrn  17904  filuni  17905  cfinfil  17913  csdfil  17914  supfil  17915  ufildr  17951  fin1aufil  17952  rnelfmlem  17972  fclsval  18028  tmdgsum  18113  tsmsfbas  18145  ust0  18237  ustn0  18238  0met  18384  xpsdsval  18399  minveclem3b  19317  evl1rhm  19937  evl1sca  19938  evl1var  19940  pf1mpf  19960  pf1ind  19963  tdeglem2  19972  deg1ldg  20003  deg1leb  20006  deg1val  20007  ulm0  20295  uhgra0  21332  uhgra0v  21333  umgra0  21348  usgra0  21378  usgra0v  21379  cusgra0v  21457  cusgra1v  21458  uvtx01vtx  21489  0wlk  21533  0trl  21534  0wlkon  21535  0trlon  21536  0pth  21558  0spth  21559  0pthon  21567  0pthonv  21569  0crct  21601  0cycl  21602  0conngra  21649  vdgr0  21659  disjdifprg  24005  esumnul  24431  prsiga  24502  derang0  24843  indispcon  24909  rdgprc  25406  dfrdg3  25408  trpredpred  25486  trpred0  25494  nosgnn0  25567  nodense  25598  fullfunfnv  25741  fullfunfv  25742  rank0  26059  ssoninhaus  26146  onint1  26147  heibor1lem  26455  heiborlem6  26462  reheibor  26485  mzpcompact2lem  26745  wopprc  27038  pw2f1ocnv  27045  pwslnmlem0  27108  fnchoice  27614  afv0fv0  27927  swrd0  28075  frgra0v  28241  2spot0  28311  bnj941  28997  bnj97  29091  bnj149  29100  bnj150  29101  bnj944  29163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator