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

Theorem 0ex 4991
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 4990. (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 4990 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 4137 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1933 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 222 . 2 𝑥 𝑥 = ∅
54issetri 3411 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1635   = wceq 1637  wex 1859  wcel 2157  Vcvv 3398  c0 4123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-nul 4990
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-dif 3779  df-nul 4124
This theorem is referenced by:  al0ssb  4992  sseliALT  4993  csbexg  4994  unisn2  4996  class2set  5031  0elpw  5033  0nep0  5035  unidif0  5037  iin0  5038  notzfaus  5039  intv  5040  snexALT  5059  p0ex  5060  dtruALT  5064  zfpair  5101  snex  5105  dtruALT2  5108  opex  5129  opthwiener  5176  0sn0ep  5235  opthprc  5374  nrelv  5453  dmsnsnsn  5832  0elon  5997  nsuceq0  6024  snsn0non  6062  iotaex  6084  nfunv  6137  fun0  6168  fvrn0  6439  fvssunirn  6440  fprg  6649  ovima0  7046  onint0  7229  tfinds2  7296  finds  7325  finds2  7327  xpexr  7339  soex  7342  supp0  7537  fvn0elsupp  7548  fvn0elsuppb  7549  brtpos0  7597  reldmtpos  7598  tfrlem16  7728  tz7.44-1  7741  seqomlem1  7784  1n0  7815  el1o  7819  om0  7837  mapdm0  8110  map0eOLD  8134  ixpexg  8172  0elixp  8179  en0  8258  ensn1  8259  en1  8262  2dom  8268  map1  8278  xp1en  8288  endisj  8289  pw2eng  8308  map2xp  8372  limensuci  8378  1sdom  8405  unxpdom2  8410  sucxpdom  8411  isinf  8415  ac6sfi  8446  fodomfi  8481  0fsupp  8539  fi0  8568  oiexg  8682  brwdom  8714  brwdom2  8720  inf3lemb  8772  infeq5i  8783  dfom3  8794  cantnfvalf  8812  cantnfval2  8816  cantnfle  8818  cantnflt  8819  cantnff  8821  cantnf0  8822  cantnfp1lem1  8825  cantnfp1lem2  8826  cantnfp1lem3  8827  cantnfp1  8828  cantnflem1a  8832  cantnflem1d  8835  cantnflem1  8836  cantnflem3  8838  cantnf  8840  cnfcomlem  8846  cnfcom  8847  cnfcom2lem  8848  cnfcom3  8851  tc0  8873  r10  8881  scottex  8998  djulcl  9022  djulf1o  9024  djuss  9032  djuun  9038  1stinl  9039  2ndinl  9040  infxpenlem  9122  fseqenlem1  9133  uncdadom  9281  cdaun  9282  cdaen  9283  cda1dif  9286  pm110.643  9287  cda0en  9289  cdacomen  9291  cdaassen  9292  xpcdaen  9293  mapcdaen  9294  cdaxpdom  9299  cdainf  9302  infcda1  9303  pwsdompw  9314  pwcdadom  9326  ackbij1lem14  9343  ackbij2lem2  9350  ackbij2lem3  9351  cf0  9361  cfeq0  9366  cfsuc  9367  cflim2  9373  isfin5  9409  isfin4-3  9425  fin1a2lem11  9520  fin1a2lem12  9521  fin1a2lem13  9522  axcc2lem  9546  ac6num  9589  zornn0g  9615  ttukeylem3  9621  brdom3  9638  iundom2g  9650  cardeq0  9662  alephadd  9687  pwcfsdom  9693  axpowndlem3  9709  canthwe  9761  canthp1lem1  9762  pwxpndom2  9775  pwcdandom  9777  gchxpidm  9779  intwun  9845  0tsk  9865  grothomex  9939  indpi  10017  fzennn  12994  hash0  13379  hashen1  13381  hashmap  13442  hashbc  13457  hashf1  13461  hashge3el3dif  13488  ccat1st1st  13629  swrdval  13643  swrd00  13644  swrd0  13661  cshfn  13763  cshnz  13765  0csh0  13766  incexclem  14793  incexc  14794  rexpen  15180  sadcf  15397  sadc0  15398  sadcp1  15399  smupf  15422  smup0  15423  smupp1  15424  0ram  15944  ram0  15946  cshws0  16023  str0  16125  ressbas  16144  ress0  16148  0rest  16298  xpscg  16426  xpscfn  16427  xpsc0  16428  xpsc1  16429  xpsfrnel  16431  xpsfrnel2  16433  xpsle  16449  ismred2  16471  acsfn  16527  0cat  16556  ciclcl  16669  cicrcl  16670  cicer  16673  setcepi  16945  0pos  17162  meet0  17345  join0  17346  mgm0b  17464  gsum0  17486  sgrp0b  17500  ga0  17935  psgn0fv0  18135  pmtrsn  18143  oppglsm  18261  efgi0  18337  vrgpf  18385  vrgpinv  18386  frgpuptinv  18388  frgpup2  18393  0frgp  18396  frgpnabllem1  18480  frgpnabllem2  18481  dprd0  18635  dmdprdpr  18653  dprdpr  18654  00lsp  19191  fvcoe1  19788  coe1f2  19790  coe1sfi  19794  coe1add  19845  coe1mul2lem1  19848  coe1mul2lem2  19849  coe1mul2  19850  ply1coe  19877  evls1rhmlem  19897  evl1sca  19909  evl1var  19911  pf1mpf  19927  pf1ind  19930  cnfldfunALT  19970  frgpcyg  20132  frlmiscvec  20402  mat0dimscm  20490  mat0dimcrng  20491  mat0scmat  20559  mavmul0  20573  mavmul0g  20574  mvmumamul1  20575  mdet0pr  20613  mdet0f1o  20614  mdet0fv0  20615  mdetunilem9  20641  d0mat2pmat  20760  chpmat0d  20856  topgele  20952  en1top  21006  en2top  21007  sn0topon  21020  indistopon  21023  indistps  21033  indistps2  21034  sn0cld  21112  indiscld  21113  neipeltop  21151  rest0  21191  restsn  21192  cmpfi  21429  refun0  21536  txindislem  21654  hmphindis  21818  xpstopnlem1  21830  xpstopnlem2  21832  ptcmpfi  21834  snfil  21885  fbasfip  21889  fgcl  21899  filconn  21904  fbasrn  21905  cfinfil  21914  csdfil  21915  supfil  21916  ufildr  21952  fin1aufil  21953  rnelfmlem  21973  fclsval  22029  tmdgsum  22116  tsmsfbas  22148  ust0  22240  ustn0  22241  0met  22388  xpsdsval  22403  minveclem3b  23417  tdeglem2  24041  deg1ldg  24072  deg1leb  24075  deg1val  24076  ulm0  24365  uhgr0  26188  upgr0eop  26229  upgr0eopALT  26231  usgr0  26357  usgr0eop  26360  lfuhgr1v0e  26368  griedg0prc  26378  0grsubgr  26392  cplgr0  26555  0grrusgr  26709  clwwlk0on0  27265  0ewlk  27293  0wlkon  27299  0trlon  27303  0pthon  27306  0pthonv  27308  0conngr  27371  konigsberglem1  27431  konigsberglem2  27432  konigsberglem3  27433  wlkl0  27553  disjdifprg  29719  disjun0  29739  fpwrelmapffslem  29840  f1ocnt  29892  resvsca  30161  locfinref  30239  esumnul  30441  esumrnmpt2  30461  prsiga  30525  ldsysgenld  30554  ldgenpisyslem1  30557  oms0  30690  carsggect  30711  eulerpartgbij  30765  eulerpartlemmf  30768  repr0  31020  breprexp  31042  bnj941  31171  bnj97  31264  bnj149  31273  bnj150  31274  bnj944  31336  derang0  31479  indispconn  31544  rdgprc  32025  dfrdg3  32027  trpredpred  32053  trpred0  32061  nosgnn0  32137  nodense  32168  nolt02o  32171  nulsslt  32234  nulssgt  32235  fullfunfnv  32379  fullfunfv  32380  rank0  32603  ssoninhaus  32769  onint1  32770  bj-0nel1  33252  bj-xpnzex  33258  bj-eltag  33277  bj-0eltag  33278  bj-tagss  33280  bj-pr1val  33304  bj-nuliota  33331  bj-nuliotaALT  33332  bj-rest10  33354  bj-rest10b  33355  bj-rest0  33359  finxpreclem1  33544  finxpreclem2  33545  finxp0  33546  finxpreclem5  33550  cnfin0  33558  cnfinltrel  33559  poimirlem28  33752  heibor1lem  33921  heiborlem6  33928  reheibor  33951  n0elqs  34415  mzpcompact2lem  37817  wopprc  38099  pw2f1ocnv  38106  pwslnmlem0  38163  pwfi2f1o  38168  relintabex  38388  clsk1indlem0  38840  clsk1indlem4  38843  clsk1indlem1  38844  fnchoice  39683  eliuniincex  39785  mapdm0OLD  39873  limsup0  40407  0cnv  40455  liminf0  40506  0cnf  40571  dvnprodlem3  40644  qndenserrnbl  40995  prsal  41018  intsal  41028  sge00  41073  sge0sn  41076  nnfoctbdjlem  41152  isomenndlem  41227  hoiqssbl  41322  ovnsubadd2lem  41342  iota0def  41658  aiota0def  41679  afv0fv0  41739  lincval0  42773  lco0  42785  linds0  42823  bnd2d  42997
  Copyright terms: Public domain W3C validator