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

Theorem 0ex 5203
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 5202. (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 5202 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 4307 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1839 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 232 . 2 𝑥 𝑥 = ∅
54issetri 3511 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1526   = wceq 1528  wex 1771  wcel 2105  Vcvv 3495  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-11 2151  ax-12 2167  ax-ext 2793  ax-nul 5202
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-nul 4291
This theorem is referenced by:  al0ssb  5204  sseliALT  5205  csbexg  5206  unisn2  5208  class2set  5246  0elpw  5248  0nep0  5250  unidif0  5252  iin0  5253  notzfaus  5254  notzfausOLD  5255  intv  5256  snexALT  5275  p0ex  5276  dtruALT  5280  zfpair  5313  snex  5323  dtruALT2  5327  opex  5348  opthwiener  5396  0sn0ep  5464  opthprc  5610  nrelv  5667  dmsnsnsn  6071  0elon  6238  nsuceq0  6265  snsn0non  6303  iotaex  6329  fun0  6413  fvrn0  6692  fvssunirn  6693  fprg  6910  ovima0  7316  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  17857  gsum0  17884  sgrp0b  17899  pwmnd  18042  mulgfval  18166  ga0  18368  psgn0fv0  18570  pmtrsn  18578  oppglsm  18698  efgi0  18777  vrgpf  18825  vrgpinv  18826  frgpuptinv  18828  frgpup2  18833  0frgp  18836  frgpnabllem1  18924  frgpnabllem2  18925  dprd0  19084  dmdprdpr  19102  dprdpr  19103  00lsp  19684  fvcoe1  20305  coe1f2  20307  coe1sfi  20311  coe1add  20362  coe1mul2lem1  20365  coe1mul2lem2  20366  coe1mul2  20367  ply1coe  20394  evls1rhmlem  20414  evl1sca  20427  evl1var  20429  pf1mpf  20445  pf1ind  20448  cnfldfunALT  20488  frgpcyg  20650  frlmiscvec  20923  mat0dimscm  21008  mat0dimcrng  21009  mat0scmat  21077  mavmul0  21091  mavmul0g  21092  mvmumamul1  21093  mdet0pr  21131  mdet0f1o  21132  mdet0fv0  21133  mdetunilem9  21159  d0mat2pmat  21276  chpmat0d  21372  en1top  21522  en2top  21523  sn0topon  21536  indistopon  21539  indistps  21549  indistps2  21550  sn0cld  21628  indiscld  21629  neipeltop  21667  rest0  21707  restsn  21708  cmpfi  21946  refun0  22053  txindislem  22171  hmphindis  22335  xpstopnlem1  22347  xpstopnlem2  22349  ptcmpfi  22351  snfil  22402  fbasfip  22406  fgcl  22416  filconn  22421  fbasrn  22422  cfinfil  22431  csdfil  22432  supfil  22433  ufildr  22469  fin1aufil  22470  rnelfmlem  22490  fclsval  22546  tmdgsum  22633  tsmsfbas  22665  ust0  22757  ustn0  22758  0met  22905  xpsdsval  22920  minveclem3b  23960  tdeglem2  24584  deg1ldg  24615  deg1leb  24618  deg1val  24619  ulm0  24908  uhgr0  26786  upgr0eop  26827  upgr0eopALT  26829  usgr0  26953  usgr0eop  26956  lfuhgr1v0e  26964  griedg0prc  26974  0grsubgr  26988  cplgr0  27135  0grrusgr  27289  clwwlk0on0  27799  0ewlk  27821  0wlkon  27827  0trlon  27831  0pthon  27834  0pthonv  27836  0conngr  27899  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  wlkl0  28074  disjdifprg  30254  disjun0  30274  fpwrelmapffslem  30395  f1ocnt  30452  resvsca  30831  locfinref  31005  esumnul  31207  esumrnmpt2  31227  prsiga  31290  ldsysgenld  31319  ldgenpisyslem1  31322  oms0  31455  carsggect  31476  eulerpartgbij  31530  eulerpartlemmf  31533  repr0  31782  breprexp  31804  bnj941  31944  bnj97  32038  bnj149  32047  bnj150  32048  bnj944  32110  derang0  32314  indispconn  32379  goeleq12bg  32494  satf0  32517  satf0op  32522  fmla0  32527  fmla0xp  32528  fmlasuc0  32529  fmlafvel  32530  fmlasuc  32531  fmlaomn0  32535  fmla0disjsuc  32543  satfdmfmla  32545  satfv0fvfmla0  32558  sate0  32560  sate0fv0  32562  sategoelfvb  32564  ex-sategoelel  32566  prv0  32575  prv1n  32576  rdgprc  32937  dfrdg3  32939  trpredpred  32965  trpred0  32973  nosgnn0  33063  nodense  33094  nolt02o  33097  nulsslt  33160  nulssgt  33161  fullfunfnv  33305  fullfunfv  33306  rank0  33529  ssoninhaus  33694  onint1  33695  bj-0nel1  34163  bj-xpnzex  34169  bj-eltag  34187  bj-0eltag  34188  bj-tagss  34190  bj-pr1val  34214  bj-nuliota  34245  bj-nuliotaALT  34246  bj-rest10  34274  bj-rest10b  34275  bj-rest0  34279  rdgssun  34542  finxpreclem1  34553  finxpreclem2  34554  finxp0  34555  finxpreclem5  34559  poimirlem28  34802  heibor1lem  34970  heiborlem6  34977  reheibor  35000  n0elqs  35466  mzpcompact2lem  39228  wopprc  39507  pw2f1ocnv  39514  pwslnmlem0  39571  pwfi2f1o  39576  clsk1indlem0  40271  clsk1indlem4  40274  clsk1indlem1  40275  mnupwd  40483  mnuprdlem1  40488  mnuprdlem2  40489  mnuprdlem3  40490  mnurnd  40499  fnchoice  41166  eliuniincex  41256  limsup0  41855  0cnv  41903  liminf0  41954  0cnf  42040  dvnprodlem3  42113  qndenserrnbl  42461  prsal  42484  intsal  42494  sge00  42539  sge0sn  42542  nnfoctbdjlem  42618  isomenndlem  42693  hoiqssbl  42788  ovnsubadd2lem  42808  iota0def  43154  aiota0def  43175  afv0fv0  43229  efmnd0nmnd  43957  efmndbas0  43958  lincval0  44368  lco0  44380  linds0  44418  bnd2d  44682
  Copyright terms: Public domain W3C validator