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

Theorem 0ex 4617
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 4616. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex ∅ ∈ V

Proof of Theorem 0ex
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 4616 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 3791 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1752 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 219 . 2 𝑥 𝑥 = ∅
54issetri 3087 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1472   = wceq 1474  wex 1694  wcel 1938  Vcvv 3077  c0 3777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-nul 4616
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-dif 3447  df-nul 3778
This theorem is referenced by:  sseliALT  4618  csbexg  4619  unisn2  4621  class2set  4657  0elpw  4659  0nep0  4661  unidif0  4663  iin0  4664  notzfaus  4665  intv  4666  snexALT  4677  p0ex  4678  dtruALT  4725  zfpair  4730  snex  4734  dtruALT2  4737  opex  4757  opthwiener  4796  opthprc  4983  dmsnsnsn  5421  0elon  5583  nsuceq0  5610  snsn0non  5648  iotaex  5670  nfunv  5720  fun0  5753  fvrn0  6009  fvssunirn  6010  fprg  6203  ovima0  6586  onint0  6763  tfinds2  6830  finds  6859  finds2  6861  xpexr  6873  soex  6876  supp0  7061  fvn0elsupp  7072  fvn0elsuppb  7073  brtpos0  7120  reldmtpos  7121  tfrlem16  7251  tz7.44-1  7264  seqomlem1  7307  1n0  7337  el1o  7341  om0  7359  map0e  7656  ixpexg  7693  0elixp  7700  en0  7780  ensn1  7781  en1  7784  2dom  7790  map1  7796  xp1en  7806  endisj  7807  pw2eng  7826  map2xp  7890  limensuci  7896  1sdom  7923  unxpdom2  7928  sucxpdom  7929  isinf  7933  ac6sfi  7964  fodomfi  7999  0fsupp  8055  fi0  8084  oiexg  8198  brwdom  8230  brwdom2  8236  inf3lemb  8280  infeq5i  8291  dfom3  8302  cantnfvalf  8320  cantnfval2  8324  cantnfle  8326  cantnflt  8327  cantnff  8329  cantnf0  8330  cantnfp1lem1  8333  cantnfp1lem2  8334  cantnfp1lem3  8335  cantnfp1  8336  cantnflem1a  8340  cantnflem1d  8343  cantnflem1  8344  cantnflem3  8346  cantnf  8348  cnfcomlem  8354  cnfcom  8355  cnfcom2lem  8356  cnfcom3  8359  tc0  8381  r10  8389  scottex  8506  infxpenlem  8594  fseqenlem1  8605  uncdadom  8751  cdaun  8752  cdaen  8753  cda1dif  8756  pm110.643  8757  cda0en  8759  cdacomen  8761  cdaassen  8762  xpcdaen  8763  mapcdaen  8764  cdaxpdom  8769  cdainf  8772  infcda1  8773  pwsdompw  8784  pwcdadom  8796  ackbij1lem14  8813  ackbij2lem2  8820  ackbij2lem3  8821  cf0  8831  cfeq0  8836  cfsuc  8837  cflim2  8843  isfin5  8879  isfin4-3  8895  fin1a2lem11  8990  fin1a2lem12  8991  fin1a2lem13  8992  axcc2lem  9016  ac6num  9059  zornn0g  9085  ttukeylem3  9091  brdom3  9106  iundom2g  9116  cardeq0  9128  alephadd  9153  pwcfsdom  9159  axpowndlem3  9175  canthwe  9227  canthp1lem1  9228  pwxpndom2  9241  pwcdandom  9243  gchxpidm  9245  intwun  9311  0tsk  9331  grothomex  9405  indpi  9483  fzennn  12496  hash0  12883  hashen1  12885  hashmap  12945  hashbc  12957  hashf1  12961  hashge3el3dif  12983  swrdval  13126  swrd00  13127  swrd0  13143  cshfn  13244  cshnz  13246  0csh0  13247  incexclem  14274  incexc  14275  rexpen  14663  sadcf  14884  sadc0  14885  sadcp1  14886  smupf  14909  smup0  14910  smupp1  14911  0ram  15444  ram0  15446  cshws0  15528  str0  15621  ressbas  15639  ress0  15643  0rest  15795  xpscg  15931  xpscfn  15932  xpsc0  15933  xpsc1  15934  xpsfrnel  15936  xpsfrnel2  15938  xpsle  15954  ismred2  15976  acsfn  16033  0cat  16062  ciclcl  16175  cicrcl  16176  cicer  16179  setcepi  16451  0pos  16667  meet0  16850  join0  16851  mgm0b  16969  gsum0  16991  sgrp0b  17005  ga0  17444  psgn0fv0  17644  pmtrsn  17652  oppglsm  17786  efgi0  17862  vrgpf  17910  vrgpinv  17911  frgpuptinv  17913  frgpup2  17918  0frgp  17921  frgpnabllem1  18004  frgpnabllem2  18005  dprd0  18158  dmdprdpr  18176  dprdpr  18177  00lsp  18704  fvcoe1  19300  coe1f2  19302  coe1sfi  19306  coe1add  19357  coe1mul2lem1  19360  coe1mul2lem2  19361  coe1mul2  19362  ply1coe  19389  evls1rhmlem  19409  evl1sca  19421  evl1var  19423  pf1mpf  19439  pf1ind  19442  frgpcyg  19645  frlmiscvec  19908  mat0dimscm  19995  mat0dimcrng  19996  mat0scmat  20064  mavmul0  20078  mavmul0g  20079  mvmumamul1  20080  mdet0pr  20118  mdet0f1o  20119  mdet0fv0  20120  mdetunilem9  20146  d0mat2pmat  20263  chpmat0d  20359  topgele  20450  en1top  20500  en2top  20501  sn0topon  20513  indistopon  20516  indistps  20526  indistps2  20527  sn0cld  20605  indiscld  20606  neipeltop  20644  rest0  20684  restsn  20685  cmpfi  20922  refun0  21029  txindislem  21147  hmphindis  21311  xpstopnlem1  21323  xpstopnlem2  21325  ptcmpfi  21327  snfil  21379  fbasfip  21383  fgcl  21393  filcon  21398  fbasrn  21399  cfinfil  21408  csdfil  21409  supfil  21410  ufildr  21446  fin1aufil  21447  rnelfmlem  21467  fclsval  21523  tmdgsum  21610  tsmsfbas  21642  ust0  21734  ustn0  21735  0met  21881  xpsdsval  21896  minveclem3b  22871  minveclem3bOLD  22883  tdeglem2  23501  deg1ldg  23532  deg1leb  23535  deg1val  23536  ulm0  23837  uhgra0  25577  uhgra0v  25578  umgra0  25593  usgra0  25638  usgra0v  25639  cusgra0v  25728  cusgra1v  25729  uvtx01vtx  25759  0wlk  25814  0trl  25815  0wlkon  25816  0trlon  25817  0pth  25839  0spth  25840  0pthon  25848  0pthonv  25850  0crct  25893  0cycl  25894  0conngra  25941  0clwlk  26032  vdgr0  26166  0egra0rgra  26202  0vgrargra  26203  frgra0v  26259  2spot0  26330  disjdifprg  28559  disjun0  28579  fpwrelmapffslem  28684  f1ocnt  28742  resvsca  28958  locfinref  29033  esumnul  29234  esumrnmpt2  29254  prsiga  29318  ldsysgenld  29347  ldgenpisyslem1  29350  oms0  29489  oms0OLD  29493  carsggect  29514  eulerpartgbij  29569  eulerpartlemmf  29572  bnj941  29943  bnj97  30036  bnj149  30045  bnj150  30046  bnj944  30108  derang0  30251  indispcon  30316  rdgprc  30787  dfrdg3  30789  trpredpred  30815  trpred0  30823  nosgnn0  30891  nodense  30924  fullfunfnv  31059  fullfunfv  31060  rank0  31283  ssoninhaus  31452  onint1  31453  bj-1ex  31963  bj-0nel1  31965  bj-xpnzex  31971  bj-eltag  31990  bj-0eltag  31991  bj-tagss  31993  bj-pr1val  32017  bj-nuliota  32042  bj-nuliotaALT  32043  bj-rest10  32054  bj-rest10b  32055  bj-rest0  32059  finxpreclem1  32234  finxpreclem2  32235  finxp0  32236  finxpreclem5  32240  poimirlem28  32482  heibor1lem  32653  heiborlem6  32660  reheibor  32683  mzpcompact2lem  36207  wopprc  36490  pw2f1ocnv  36497  pwslnmlem0  36554  pwfi2f1o  36559  relintabex  36788  clsk1indlem0  37241  clsk1indlem4  37244  clsk1indlem1  37245  fnchoice  38093  eliuniincex  38206  mapdm0  38262  0cnf  38649  dvnprodlem3  38728  qndenserrnbl  39085  prsal  39108  intsal  39118  sge00  39163  sge0sn  39166  nnfoctbdjlem  39242  isomenndlem  39314  hoiqssbl  39409  ovnsubadd2lem  39429  afv0fv0  39773  vtxval0  40362  iedgval0  40363  uhgr0  40390  upgr0eop  40431  upgr0eopALT  40433  usgr0  40561  usgr0eop  40564  lfuhgr1v0e  40572  griedg0prc  40580  0grsubgr  40594  cplgr0  40739  0grrusgr  40871  0ewlk  41374  01wlk  41376  0wlkOn  41380  0Trl  41382  0TrlOn  41384  0pth-av  41385  0spth-av  41386  0pthon-av  41387  0pthonv-av  41389  0Crct  41392  0Cycl  41393  0conngr  41451  eupth0  41474  konigsberglem1  41514  konigsberglem2  41515  konigsberglem3  41516  lincval0  42090  lco0  42102  linds0  42140
  Copyright terms: Public domain W3C validator