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

Theorem 0ex 5269
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 5268. (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 5268 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 4308 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1851 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 230 . 2 𝑥 𝑥 = ∅
54issetri 3464 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1540   = wceq 1542  wex 1782  wcel 2107  Vcvv 3448  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5268
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-nul 4288
This theorem is referenced by:  al0ssb  5270  sseliALT  5271  csbexg  5272  unisn2  5274  class2set  5315  0elpw  5316  0nep0  5318  unidif0  5320  iin0  5322  notzfaus  5323  intv  5324  snexALT  5343  p0ex  5344  dtruALT  5348  zfpair  5381  snex  5393  opex  5426  opthwiener  5476  0sn0ep  5546  opthprc  5701  nrelv  5761  dmsnsnsn  6177  0elon  6376  nsuceq0  6405  snsn0non  6447  iotaex  6474  iotaexOLD  6481  fun0  6571  fvrn0  6877  fvssunirnOLD  6881  fprg  7106  ovima0  7538  onint0  7731  tfinds2  7805  finds  7840  finds2  7842  xpexr  7860  soex  7863  supp0  8102  fvn0elsupp  8116  fvn0elsuppb  8117  brtpos0  8169  reldmtpos  8170  tfrlem16  8344  tz7.44-1  8357  seqomlem1  8401  1n0  8439  nlim1  8440  nlim2  8441  el1o  8446  om0  8468  mapdm0  8787  fsetexb  8809  0map0sn0  8830  ixpexg  8867  0elixp  8874  en0  8964  en0OLD  8965  en0ALT  8966  en0r  8967  ensn1  8968  ensn1OLD  8969  en1  8972  en1OLD  8973  2dom  8981  map1  8991  enpr2d  9000  xp1en  9008  endisj  9009  pw2eng  9029  0domg  9051  map2xp  9098  limensuci  9104  snnen2o  9188  0sdom1dom  9189  rex2dom  9197  1sdom2dom  9198  1sdomOLD  9200  unxpdom2  9205  sucxpdom  9206  isinf  9211  isinfOLD  9212  ac6sfi  9238  fodomfi  9276  0fsupp  9334  fi0  9363  oiexg  9478  brwdom  9510  brwdom2  9516  inf3lemb  9568  infeq5i  9579  dfom3  9590  cantnfvalf  9608  cantnfval2  9612  cantnfle  9614  cantnflt  9615  cantnff  9617  cantnf0  9618  cantnfp1lem1  9621  cantnfp1lem3  9623  cantnfp1  9624  cantnflem1a  9628  cantnflem1d  9631  cantnflem1  9632  cantnf  9636  cnfcomlem  9642  cnfcom  9643  cnfcom2lem  9644  cnfcom3  9647  ssttrcl  9658  ttrcltr  9659  ttrclss  9663  dmttrcl  9664  ttrclselem2  9669  tc0  9690  r10  9711  scottex  9828  djulcl  9853  djulf1o  9855  djuss  9863  djuun  9869  1stinl  9870  2ndinl  9871  infxpenlem  9956  fseqenlem1  9967  undjudom  10110  endjudisj  10111  djuen  10112  dju1dif  10115  dju1p1e2  10116  dju0en  10118  djucomen  10120  djuassen  10121  xpdjuen  10122  mapdjuen  10123  djuxpdom  10128  djuinf  10131  infdju1  10132  djulepw  10135  pwsdompw  10147  pwdjudom  10159  ackbij1lem14  10176  ackbij2lem2  10183  ackbij2lem3  10184  cf0  10194  cfeq0  10199  cfsuc  10200  cflim2  10206  isfin5  10242  isfin4p1  10258  fin1a2lem11  10353  fin1a2lem12  10354  fin1a2lem13  10355  axcc2lem  10379  ac6num  10422  zornn0g  10448  ttukeylem3  10454  brdom3  10471  iundom2g  10483  cardeq0  10495  pwcfsdom  10526  axpowndlem3  10542  canthwe  10594  canthp1lem1  10595  pwxpndom2  10608  pwdjundom  10610  gchxpidm  10612  intwun  10678  0tsk  10698  grothomex  10772  indpi  10850  fzennn  13880  hash0  14274  hashen1  14277  hashmap  14342  hashbc  14357  hashf1  14363  hashge3el3dif  14392  ccat1st1st  14523  swrdval  14538  swrd00  14539  swrd0  14553  cshfn  14685  cshnz  14687  0csh0  14688  incexclem  15728  incexc  15729  rexpen  16117  sadcf  16340  sadc0  16341  sadcp1  16342  smupf  16365  smup0  16366  smupp1  16367  0ram  16899  ram0  16901  cshws0  16981  str0  17068  ressbasOLD  17126  ress0  17131  0rest  17318  fnpr2ob  17447  xpsfrnel  17451  xpsle  17468  ismred2  17490  acsfn  17546  0cat  17576  ciclcl  17692  cicrcl  17693  cicer  17696  setcepi  17981  setc2obas  17987  setc2ohom  17988  cat1  17990  0pos  18217  0posOLD  18218  join0  18301  meet0  18302  mgm0b  18519  gsum0  18546  sgrp0b  18561  efmnd0nmnd  18707  pwmnd  18754  mulgfval  18881  ga0  19085  psgn0fv0  19300  pmtrsn  19308  oppglsm  19431  efgi0  19509  vrgpf  19557  vrgpinv  19558  frgpuptinv  19560  frgpup2  19565  0frgp  19568  frgpnabllem1  19658  frgpnabllem2  19659  dprd0  19817  dmdprdpr  19835  dprdpr  19836  00lsp  20458  cnfldfun  20824  frgpcyg  20996  frlmiscvec  21271  fvcoe1  21594  coe1f2  21596  coe1sfi  21600  coe1add  21651  coe1mul2lem1  21654  coe1mul2lem2  21655  coe1mul2  21656  ply1coe  21683  evls1rhmlem  21703  evl1sca  21716  evl1var  21718  pf1mpf  21734  pf1ind  21737  mat0dimscm  21834  mat0dimcrng  21835  mat0scmat  21903  mavmul0  21917  mavmul0g  21918  mvmumamul1  21919  mdet0pr  21957  mdet0f1o  21958  mdet0fv0  21959  mdetunilem9  21985  d0mat2pmat  22103  chpmat0d  22199  en1top  22350  en2top  22351  sn0topon  22364  indistopon  22367  indistps  22377  indistps2  22378  sn0cld  22457  indiscld  22458  neipeltop  22496  rest0  22536  restsn  22537  cmpfi  22775  refun0  22882  txindislem  23000  hmphindis  23164  xpstopnlem1  23176  xpstopnlem2  23178  ptcmpfi  23180  snfil  23231  fbasfip  23235  fgcl  23245  filconn  23250  fbasrn  23251  cfinfil  23260  csdfil  23261  supfil  23262  ufildr  23298  fin1aufil  23299  rnelfmlem  23319  fclsval  23375  tmdgsum  23462  tsmsfbas  23495  ust0  23587  ustn0  23588  0met  23735  xpsdsval  23750  minveclem3b  24808  tdeglem2  25442  deg1ldg  25473  deg1leb  25476  deg1val  25477  ulm0  25766  nosgnn0  27022  nodense  27056  nolt02o  27059  nogt01o  27060  nulsslt  27158  nulssgt  27159  bday1s  27192  made0  27225  uhgr0  28066  upgr0eop  28107  upgr0eopALT  28109  usgr0  28233  usgr0eop  28236  lfuhgr1v0e  28244  griedg0prc  28254  0grsubgr  28268  cplgr0  28415  0grrusgr  28569  clwwlk0on0  29078  0ewlk  29100  0wlkon  29106  0trlon  29110  0pthon  29113  0pthonv  29115  0conngr  29178  konigsberglem1  29238  konigsberglem2  29239  konigsberglem3  29240  wlkl0  29353  disjdifprg  31535  disjun0  31555  fpwrelmapffslem  31691  f1ocnt  31747  resvsca  32161  locfinref  32462  zarcmplem  32502  esumnul  32687  esumrnmpt2  32707  prsiga  32770  ldsysgenld  32799  ldgenpisyslem1  32802  oms0  32937  carsggect  32958  eulerpartgbij  33012  eulerpartlemmf  33015  repr0  33264  breprexp  33286  bnj941  33424  bnj97  33518  bnj149  33527  bnj150  33528  bnj944  33590  fineqvac  33738  derang0  33803  indispconn  33868  goeleq12bg  33983  satf0  34006  satf0op  34011  fmla0  34016  fmla0xp  34017  fmlasuc0  34018  fmlafvel  34019  fmlasuc  34020  fmlaomn0  34024  fmla0disjsuc  34032  satfdmfmla  34034  satfv0fvfmla0  34047  sate0  34049  sate0fv0  34051  sategoelfvb  34053  ex-sategoelel  34055  prv0  34064  prv1n  34065  rdgprc  34408  dfrdg3  34410  fullfunfnv  34560  fullfunfv  34561  rank0  34784  ssoninhaus  34949  onint1  34950  bj-0nel1  35453  bj-xpnzex  35459  bj-eltag  35477  bj-0eltag  35478  bj-tagss  35480  bj-pr1val  35504  bj-snex  35535  bj-snfromadj  35544  bj-nuliota  35557  bj-nuliotaALT  35558  bj-rdg0gALT  35571  bj-rest10  35588  bj-rest10b  35589  bj-rest0  35593  rdgssun  35878  finxpreclem1  35889  finxpreclem2  35890  finxp0  35891  finxpreclem5  35895  poimirlem28  36135  heibor1lem  36297  heiborlem6  36304  reheibor  36327  n0elqs  36816  sticksstones11  40593  mzpcompact2lem  41103  wopprc  41383  pw2f1ocnv  41390  pwslnmlem0  41447  pwfi2f1o  41452  2omomeqom  41667  cantnfub  41685  cantnfresb  41688  omcl3g  41698  nadd1suc  41737  naddwordnexlem4  41747  nla0002  41770  nla0003  41771  nla0001  41772  clsk1indlem0  42387  clsk1indlem4  42390  clsk1indlem1  42391  mnupwd  42621  mnuprdlem1  42626  mnuprdlem2  42627  mnuprdlem3  42628  mnurnd  42637  fnchoice  43308  eliuniincex  43393  limsup0  44009  0cnv  44057  liminf0  44108  0cnf  44192  dvnprodlem3  44263  qndenserrnbl  44610  prsal  44633  intsal  44645  sge00  44691  sge0sn  44694  nnfoctbdjlem  44770  isomenndlem  44845  hoiqssbl  44940  ovnsubadd2lem  44960  upwordnul  45193  iota0def  45346  aiota0def  45402  afv0fv0  45455  0nelsetpreimafv  45656  lincval0  46570  lco0  46582  linds0  46620  0aryfvalel  46794  0aryfvalelfv  46795  1aryenef  46805  2aryenef  46816  mof0  46978  0thinc  47145  setc2othin  47150  prstcthin  47170  bnd2d  47200
  Copyright terms: Public domain W3C validator