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

Theorem 0ex 5208
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 5207. (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 5207 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 4312 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1841 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 232 . 2 𝑥 𝑥 = ∅
54issetri 3516 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1528   = wceq 1530  wex 1773  wcel 2107  Vcvv 3500  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-11 2153  ax-12 2169  ax-ext 2798  ax-nul 5207
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-nul 4296
This theorem is referenced by:  al0ssb  5209  sseliALT  5210  csbexg  5211  unisn2  5213  class2set  5251  0elpw  5253  0nep0  5255  unidif0  5257  iin0  5258  notzfaus  5259  notzfausOLD  5260  intv  5261  snexALT  5280  p0ex  5281  dtruALT  5285  zfpair  5318  snex  5328  dtruALT2  5332  opex  5353  opthwiener  5401  0sn0ep  5469  opthprc  5615  nrelv  5672  dmsnsnsn  6075  0elon  6242  nsuceq0  6269  snsn0non  6307  iotaex  6333  fun0  6416  fvrn0  6695  fvssunirn  6696  fprg  6913  ovima0  7317  onint0  7499  tfinds2  7566  finds  7596  finds2  7598  xpexr  7611  soex  7614  supp0  7826  fvn0elsupp  7837  fvn0elsuppb  7838  brtpos0  7890  reldmtpos  7891  tfrlem16  8020  tz7.44-1  8033  seqomlem1  8077  1n0  8110  el1o  8115  om0  8133  mapdm0  8411  ixpexg  8475  0elixp  8482  en0  8561  ensn1  8562  en1  8565  2dom  8571  map1  8581  xp1en  8592  endisj  8593  pw2eng  8612  map2xp  8676  limensuci  8682  1sdom  8710  unxpdom2  8715  sucxpdom  8716  isinf  8720  ac6sfi  8751  fodomfi  8786  0fsupp  8844  fi0  8873  oiexg  8988  brwdom  9020  brwdom2  9026  inf3lemb  9077  infeq5i  9088  dfom3  9099  cantnfvalf  9117  cantnfval2  9121  cantnfle  9123  cantnflt  9124  cantnff  9126  cantnf0  9127  cantnfp1lem1  9130  cantnfp1lem3  9132  cantnfp1  9133  cantnflem1a  9137  cantnflem1d  9140  cantnflem1  9141  cantnf  9145  cnfcomlem  9151  cnfcom  9152  cnfcom2lem  9153  cnfcom3  9156  tc0  9178  r10  9186  scottex  9303  djulcl  9328  djulf1o  9330  djuss  9338  djuun  9344  1stinl  9345  2ndinl  9346  infxpenlem  9428  fseqenlem1  9439  undjudom  9582  endjudisj  9583  djuen  9584  dju1dif  9587  dju1p1e2  9588  dju0en  9590  djucomen  9592  djuassen  9593  xpdjuen  9594  mapdjuen  9595  djuxpdom  9600  djuinf  9603  infdju1  9604  djulepw  9607  pwsdompw  9615  pwdjudom  9627  ackbij1lem14  9644  ackbij2lem2  9651  ackbij2lem3  9652  cf0  9662  cfeq0  9667  cfsuc  9668  cflim2  9674  isfin5  9710  isfin4p1  9726  fin1a2lem11  9821  fin1a2lem12  9822  fin1a2lem13  9823  axcc2lem  9847  ac6num  9890  zornn0g  9916  ttukeylem3  9922  brdom3  9939  iundom2g  9951  cardeq0  9963  pwcfsdom  9994  axpowndlem3  10010  canthwe  10062  canthp1lem1  10063  pwxpndom2  10076  pwdjundom  10078  gchxpidm  10080  intwun  10146  0tsk  10166  grothomex  10240  indpi  10318  fzennn  13326  hash0  13718  hashen1  13721  hashmap  13786  hashbc  13801  hashf1  13805  hashge3el3dif  13834  ccat1st1st  13974  swrdval  13995  swrd00  13996  swrd0  14010  cshfn  14142  cshnz  14144  0csh0  14145  incexclem  15181  incexc  15182  rexpen  15571  sadcf  15792  sadc0  15793  sadcp1  15794  smupf  15817  smup0  15818  smupp1  15819  0ram  16346  ram0  16348  cshws0  16425  str0  16525  ressbas  16544  ress0  16548  0rest  16693  fnpr2ob  16821  xpsfrnel  16825  xpsle  16842  ismred2  16864  acsfn  16920  0cat  16949  ciclcl  17062  cicrcl  17063  cicer  17066  setcepi  17338  0pos  17554  meet0  17737  join0  17738  mgm0b  17856  gsum0  17883  sgrp0b  17898  mulgfval  18156  ga0  18358  psgn0fv0  18559  pmtrsn  18567  oppglsm  18687  efgi0  18766  vrgpf  18814  vrgpinv  18815  frgpuptinv  18817  frgpup2  18822  0frgp  18825  frgpnabllem1  18913  frgpnabllem2  18914  dprd0  19073  dmdprdpr  19091  dprdpr  19092  00lsp  19673  fvcoe1  20294  coe1f2  20296  coe1sfi  20300  coe1add  20351  coe1mul2lem1  20354  coe1mul2lem2  20355  coe1mul2  20356  ply1coe  20383  evls1rhmlem  20403  evl1sca  20416  evl1var  20418  pf1mpf  20434  pf1ind  20437  cnfldfunALT  20477  frgpcyg  20639  frlmiscvec  20912  mat0dimscm  20997  mat0dimcrng  20998  mat0scmat  21066  mavmul0  21080  mavmul0g  21081  mvmumamul1  21082  mdet0pr  21120  mdet0f1o  21121  mdet0fv0  21122  mdetunilem9  21148  d0mat2pmat  21265  chpmat0d  21361  en1top  21511  en2top  21512  sn0topon  21525  indistopon  21528  indistps  21538  indistps2  21539  sn0cld  21617  indiscld  21618  neipeltop  21656  rest0  21696  restsn  21697  cmpfi  21935  refun0  22042  txindislem  22160  hmphindis  22324  xpstopnlem1  22336  xpstopnlem2  22338  ptcmpfi  22340  snfil  22391  fbasfip  22395  fgcl  22405  filconn  22410  fbasrn  22411  cfinfil  22420  csdfil  22421  supfil  22422  ufildr  22458  fin1aufil  22459  rnelfmlem  22479  fclsval  22535  tmdgsum  22622  tsmsfbas  22654  ust0  22746  ustn0  22747  0met  22894  xpsdsval  22909  minveclem3b  23949  tdeglem2  24573  deg1ldg  24604  deg1leb  24607  deg1val  24608  ulm0  24897  uhgr0  26775  upgr0eop  26816  upgr0eopALT  26818  usgr0  26942  usgr0eop  26945  lfuhgr1v0e  26953  griedg0prc  26963  0grsubgr  26977  cplgr0  27124  0grrusgr  27278  clwwlk0on0  27788  0ewlk  27810  0wlkon  27816  0trlon  27820  0pthon  27823  0pthonv  27825  0conngr  27888  konigsberglem1  27948  konigsberglem2  27949  konigsberglem3  27950  wlkl0  28063  disjdifprg  30243  disjun0  30263  fpwrelmapffslem  30384  f1ocnt  30441  resvsca  30820  locfinref  30994  esumnul  31196  esumrnmpt2  31216  prsiga  31279  ldsysgenld  31308  ldgenpisyslem1  31311  oms0  31444  carsggect  31465  eulerpartgbij  31519  eulerpartlemmf  31522  repr0  31771  breprexp  31793  bnj941  31933  bnj97  32027  bnj149  32036  bnj150  32037  bnj944  32099  derang0  32303  indispconn  32368  goeleq12bg  32483  satf0  32506  satf0op  32511  fmla0  32516  fmla0xp  32517  fmlasuc0  32518  fmlafvel  32519  fmlasuc  32520  fmlaomn0  32524  fmla0disjsuc  32532  satfdmfmla  32534  satfv0fvfmla0  32547  sate0  32549  sate0fv0  32551  sategoelfvb  32553  ex-sategoelel  32555  prv0  32564  prv1n  32565  rdgprc  32926  dfrdg3  32928  trpredpred  32954  trpred0  32962  nosgnn0  33052  nodense  33083  nolt02o  33086  nulsslt  33149  nulssgt  33150  fullfunfnv  33294  fullfunfv  33295  rank0  33518  ssoninhaus  33683  onint1  33684  bj-0nel1  34152  bj-xpnzex  34158  bj-eltag  34176  bj-0eltag  34177  bj-tagss  34179  bj-pr1val  34203  bj-nuliota  34234  bj-nuliotaALT  34235  bj-rest10  34263  bj-rest10b  34264  bj-rest0  34268  rdgssun  34531  finxpreclem1  34542  finxpreclem2  34543  finxp0  34544  finxpreclem5  34548  poimirlem28  34790  heibor1lem  34958  heiborlem6  34965  reheibor  34988  n0elqs  35454  mzpcompact2lem  39216  wopprc  39495  pw2f1ocnv  39502  pwslnmlem0  39559  pwfi2f1o  39564  clsk1indlem0  40259  clsk1indlem4  40262  clsk1indlem1  40263  mnupwd  40471  mnuprdlem1  40476  mnuprdlem2  40477  mnuprdlem3  40478  mnurnd  40487  fnchoice  41154  eliuniincex  41244  limsup0  41843  0cnv  41891  liminf0  41942  0cnf  42028  dvnprodlem3  42101  qndenserrnbl  42449  prsal  42472  intsal  42482  sge00  42527  sge0sn  42530  nnfoctbdjlem  42606  isomenndlem  42681  hoiqssbl  42776  ovnsubadd2lem  42796  iota0def  43142  aiota0def  43163  afv0fv0  43217  lincval0  44305  lco0  44317  linds0  44355  bnd2d  44619
  Copyright terms: Public domain W3C validator