Theorem 0ex 5267

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 5266. (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.

Step	Hyp	Ref	Expression
1		ax-nul 5266	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4300	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3473	1 ⊢ ∅ ∈ V

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-nul 4282

This theorem is used by:  al0ssb  5268  sseliALT  5269  csbexg  5270  unisn2  5272  class2set  5323  0elpw  5324  0nep0  5326  unidif0  5328  unidif0OLD  5329  iin0  5331  notsep  5332  intv  5333  snexALT  5352  p0ex  5353  dtruALT  5357  zfpair  5390  snexOLD  5407  opexOLD  5440  opthwiener  5494  0sn0ep  5562  opthprc  5722  nrelv  5786  nrelvOLD  5787  dmsnsnsn  6240  0elon  6444  nsuceq0  6474  snsn0non  6515  iotaex  6541  fun0  6635  fvrn0  6944  fprg  7191  ovima0  7632  onint0  7839  tfinds2  7909  finds  7942  finds2  7944  xpexr  7964  soex  7967  supp0  8220  fvn0elsupp  8235  fvn0elsuppb  8236  brtpos0  8288  reldmtpos  8289  tfrlem16  8439  tz7.44-1  8452  seqomlem1  8498  1n0OLD  8534  nlim1  8535  nlim2  8536  el1o  8541  om0  8563  mapdm0  8900  fsetexb  8924  0map0sn0  8951  ixpexg  8988  0elixp  8995  en0  9083  en0ALT  9084  en0r  9085  ensn1  9086  en1  9089  2dom  9096  map1  9106  enpr2d  9114  xp1en  9120  endisj  9121  pw2eng  9140  0domg  9161  map2xp  9204  limensuci  9210  snnen2o  9274  0sdom1dom  9275  rex2dom  9282  1sdom2dom  9283  unxpdom2  9289  sucxpdom  9290  isinf  9294  ac6sfi  9313  fodomfi  9342  0fsupp  9419  fi0  9449  oiexg  9566  brwdom  9598  brwdom2  9604  inf3lemb  9663  infeq5i  9674  dfom3  9685  cantnfvalf  9703  cantnfval2  9707  cantnfle  9709  cantnflt  9710  cantnff  9712  cantnf0  9713  cantnfp1lem1  9716  cantnfp1lem3  9718  cantnfp1  9719  cantnflem1a  9723  cantnflem1d  9726  cantnflem1  9727  cantnf  9731  cnfcomlem  9737  cnfcom  9738  cnfcom2lem  9739  cnfcom3  9742  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  dmttrcl  9759  ttrclselem2  9764  tc0  9783  r10  9812  scottex  9970  scottexOLD  9971  bnd2d  10005  djulcl  10028  djulf1o  10030  djuss  10038  djuun  10044  1stinl  10045  2ndinl  10046  infxpenlem  10131  fseqenlem1  10142  undjudom  10285  endjudisj  10286  djuen  10287  dju1dif  10290  dju1p1e2  10291  dju0en  10293  djucomen  10295  djuassen  10296  xpdjuen  10297  mapdjuen  10298  djuxpdom  10303  djuinf  10306  infdju1  10307  djulepw  10310  pwsdompw  10320  pwdjudom  10332  ackbij1lem14  10349  ackbij2lem2  10356  ackbij2lem3  10357  cf0  10367  cfeq0  10373  cfsuc  10374  isfin5  10416  isfin4p1  10432  fin1a2lem11  10527  fin1a2lem12  10528  fin1a2lem13  10529  axcc2lem  10553  ac6num  10596  zornn0g  10622  ttukeylem3  10628  brdom3  10646  iundom2g  10663  cardeq0  10675  pwcfsdom  10707  axpowndlem3  10723  canthwe  10775  canthp1lem1  10776  pwxpndom2  10789  pwdjundom  10791  gchxpidm  10793  intwun  10859  0tsk  10879  grothomex  10953  indpi  11031  fzennn  14151  hash0  14552  hashen1  14555  hashmap  14621  hashbc  14639  hashf1  14643  hashge3el3dif  14673  ccat1st1st  14818  swrdval  14833  swrd00  14834  swrd0  14850  cshfn  14983  cshnz  14985  0csh0  14986  incexclem  16049  incexc  16050  rexpen  16440  sadcf  16667  sadc0  16668  sadcp1  16669  smupf  16692  smup0  16693  smupp1  16694  0ram  17242  ram0  17244  cshws0  17323  str0  17411  ress0  17465  0rest  17650  fnpr2ob  17780  xpsfrnel  17784  xpsle  17801  ismred2  17823  acsfn  17883  0cat  17913  ciclcl  18027  cicrcl  18028  cicer  18031  setcepi  18313  setc2obas  18319  setc2ohom  18320  cat1  18322  0pos  18545  join0  18627  meet0  18628  mgm0b  18885  gsum0  18923  sgrp0b  18967  efmnd0nmnd  19136  degenmgmopdm  19184  degenmgmnfn  19186  degenmgm  19187  degenmgm2  19190  pwmnd  19193  mulgfval  19329  ga0  19563  psgn0fv0  19776  pmtrsn  19784  oppglsm  19907  efgi0  19985  vrgpf  20033  vrgpinv  20034  frgpuptinv  20036  frgpup2  20041  0frgp  20044  frgpnabllem1  20138  frgpnabllem2  20139  dprd0  20298  dmdprdpr  20316  dprdpr  20317  00lsp  21307  cnfldfun  21744  frgpcyg  21934  frlmiscvec  22210  fvcoe1  22580  coe1f2  22582  coe1sfi  22586  coe1add  22638  coe1mul2lem1  22641  coe1mul2lem2  22642  coe1mul2  22643  ply1coe  22671  evls1rhmlem  22694  evl1sca  22707  evl1var  22709  pf1mpf  22725  pf1ind  22728  mat0dimscm  22839  mat0dimcrng  22840  mat0scmat  22908  mavmul0  22922  mavmul0g  22923  mvmumamul1  22924  mdet0pr  22962  mdet0f1o  22963  mdet0fv0  22964  mdetunilem9  22990  d0mat2pmat  23111  chpmat0d  23207  en1top  23357  en2top  23358  sn0topon  23371  indistopon  23374  indistps  23384  indistps2  23385  sn0cld  23463  indiscld  23464  neipeltop  23502  rest0  23542  restsn  23543  cmpfi  23781  refun0  23889  txindislem  24007  hmphindis  24171  xpstopnlem1  24183  xpstopnlem2  24185  ptcmpfi  24187  snfil  24238  fbasfip  24242  fgcl  24252  filconn  24257  fbasrn  24258  cfinfil  24267  csdfil  24268  supfil  24269  ufildr  24305  fin1aufil  24306  rnelfmlem  24326  fclsval  24382  tmdgsum  24469  tsmsfbas  24502  ust0  24594  ustn0  24595  0met  24740  xpsdsval  24755  minveclem3b  25804  tdeglem2  26434  deg1ldg  26465  deg1leb  26468  deg1val  26469  ulm0  26775  nosgnn0  28072  nodense  28106  nolt02o  28109  nogt01o  28110  nulslts  28218  nulsgts  28219  bday1  28257  made0  28306  precsexlem1  28650  precsexlem2  28651  uhgr0  29708  upgr0eop  29749  upgr0eopALT  29751  usgr0  29881  usgr0eop  29884  lfuhgr1v0e  29892  griedg0prc  29902  0grsubgr  29916  cplgr0  30063  0grrusgr  30217  clwwlk0on0  30740  0ewlk  30762  0wlkon  30768  0trlon  30772  0pthon  30775  0pthonv  30777  0conngr  30850  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  wlkl0  31025  disjdifprg  33267  disjun0  33287  of0r  33370  fpwrelmapffslem  33420  f1ocnt  33488  resvsca  33997  1arithidom  34173  0mplrim  34257  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhm0  34269  mplidomlem  34270  vieta  34323  locfinref  34584  zarcmplem  34624  esumnul  34791  esumrnmpt2  34811  prsiga  34874  ldsysgenld  34904  ldgenpisyslem1  34907  oms0  35040  carsggect  35061  eulerpartgbij  35115  eulerpartlemmf  35118  repr0  35351  breprexp  35373  bnj941  35514  bnj97  35607  bnj149  35616  bnj150  35617  bnj944  35679  fineqvac  35925  fineqvnttrclse  35933  kard0  35963  kard0b  35968  wevgblacfn  36080  derang0  36142  indispconn  36207  goeleq12bg  36322  satf0  36345  satf0op  36350  fmla0  36355  fmla0xp  36356  fmlasuc0  36357  fmlafvel  36358  fmlasuc  36359  fmlaomn0  36363  fmla0disjsuc  36371  satfdmfmla  36373  satfv0fvfmla0  36386  sate0  36388  sate0fv0  36390  sategoelfvb  36392  ex-sategoelel  36394  prv0  36403  prv1n  36404  elpssex  36672  elpssmo  36673  rdgprc  36771  dfrdg3  36773  fullfunfnv  36925  fullfunfv  36926  rank0  37146  nmulrid  37161  ssoninhaus  37451  onint1  37452  mh-infprim2bi  37550  bj-0nel1  38081  bj-xpnzex  38087  bj-eltag  38105  bj-0eltag  38106  bj-tagss  38108  bj-pr1val  38132  bj-snex  38163  bj-snfromadj  38172  bj-nuliota  38242  bj-nuliotaALT  38243  bj-rdg0gALT  38256  bj-rest10  38279  bj-rest10b  38280  bj-rest0  38284  bj-pr0moore  38307  rdgssun  38569  finxpreclem1  38580  finxpreclem2  38581  finxp0  38582  finxpreclem5  38586  poimirlem28  38834  varprop  38910  heibor1lem  39009  heiborlem6  39016  reheibor  39039  n0elqs  39530  sticksstones11  43472  mzpcompact2lem  44028  wopprc  44303  pw2f1ocnv  44310  pwslnmlem0  44359  pwfi2f1o  44364  2omomeqom  44566  cantnfub  44584  cantnfresb  44587  omcl3g  44597  nadd1suc  44655  naddwordnexlem4  44664  nla0002  44686  nla0003  44687  nla0001  44688  clsk1indlem0  45302  clsk1indlem4  45305  clsk1indlem1  45306  mnupwd  45512  mnuprdlem1  45517  mnuprdlem2  45518  mnuprdlem3  45519  mnurnd  45528  permaxnul  46262  permaxinf2lem  46266  nregmodelf1o  46269  nregmodellem  46270  nregmodel  46271  fnchoice  46320  eliuniincex  46397  limsup0  46977  0cnv  47025  liminf0  47076  0cnf  47160  dvnprodlem3  47231  qndenserrnbl  47578  prsal  47601  intsal  47613  sge00  47659  sge0sn  47662  nnfoctbdjlem  47738  isomenndlem  47813  hoiqssbl  47908  ovnsubadd2lem  47928  iota0def  48381  aiota0def  48439  afv0fv0  48492  0nelsetpreimafv  48745  lincval0  49858  lco0  49870  linds0  49908  0aryfvalel  50077  0aryfvalelfv  50078  1aryenef  50088  2aryenef  50099  mof0  50280  dftpos5  50318  dftpos6  50319  relcic  50490  discsubclem  50508  discsubc  50509  iinfconstbas  50511  nelsubclem  50512  0funcg  50531  0func  50533  0funcALT  50534  oppffn  50571  oppfvalg  50573  fucofvalne  50778  0thinc  50925  setc2othin  50932  setc1ohomfval  50959  setc1ocofval  50960  isinito2lem  50964  prstcthin  51030  setc1onsubc  51071  parhomval  51074  parswapval  51107  parswapprop  51108  par2hom  51110  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114  initocmd  51183  termolmd  51184