Theorem 0ex 5306

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 5305. (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 5305	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4342	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3490	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3474  ∅c0 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-nul 4322

This theorem is referenced by:  al0ssb  5307  sseliALT  5308  csbexg  5309  unisn2  5311  class2set  5352  0elpw  5353  0nep0  5355  unidif0  5357  iin0  5359  notzfaus  5360  intv  5361  snexALT  5380  p0ex  5381  dtruALT  5385  zfpair  5418  snex  5430  opex  5463  opthwiener  5513  0sn0ep  5583  opthprc  5738  nrelv  5798  dmsnsnsn  6216  0elon  6415  nsuceq0  6444  snsn0non  6486  iotaex  6513  iotaexOLD  6520  fun0  6610  fvrn0  6918  fvssunirnOLD  6922  fprg  7149  ovima0  7582  onint0  7775  tfinds2  7849  finds  7885  finds2  7887  xpexr  7905  soex  7908  supp0  8147  fvn0elsupp  8161  fvn0elsuppb  8162  brtpos0  8214  reldmtpos  8215  tfrlem16  8389  tz7.44-1  8402  seqomlem1  8446  1n0  8484  nlim1  8485  nlim2  8486  el1o  8491  om0  8513  mapdm0  8832  fsetexb  8854  0map0sn0  8875  ixpexg  8912  0elixp  8919  en0  9009  en0OLD  9010  en0ALT  9011  en0r  9012  ensn1  9013  ensn1OLD  9014  en1  9017  en1OLD  9018  2dom  9026  map1  9036  enpr2d  9045  xp1en  9053  endisj  9054  pw2eng  9074  0domg  9096  map2xp  9143  limensuci  9149  snnen2o  9233  0sdom1dom  9234  rex2dom  9242  1sdom2dom  9243  1sdomOLD  9245  unxpdom2  9250  sucxpdom  9251  isinf  9256  isinfOLD  9257  ac6sfi  9283  fodomfi  9321  0fsupp  9381  fi0  9411  oiexg  9526  brwdom  9558  brwdom2  9564  inf3lemb  9616  infeq5i  9627  dfom3  9638  cantnfvalf  9656  cantnfval2  9660  cantnfle  9662  cantnflt  9663  cantnff  9665  cantnf0  9666  cantnfp1lem1  9669  cantnfp1lem3  9671  cantnfp1  9672  cantnflem1a  9676  cantnflem1d  9679  cantnflem1  9680  cantnf  9684  cnfcomlem  9690  cnfcom  9691  cnfcom2lem  9692  cnfcom3  9695  ssttrcl  9706  ttrcltr  9707  ttrclss  9711  dmttrcl  9712  ttrclselem2  9717  tc0  9738  r10  9759  scottex  9876  djulcl  9901  djulf1o  9903  djuss  9911  djuun  9917  1stinl  9918  2ndinl  9919  infxpenlem  10004  fseqenlem1  10015  undjudom  10158  endjudisj  10159  djuen  10160  dju1dif  10163  dju1p1e2  10164  dju0en  10166  djucomen  10168  djuassen  10169  xpdjuen  10170  mapdjuen  10171  djuxpdom  10176  djuinf  10179  infdju1  10180  djulepw  10183  pwsdompw  10195  pwdjudom  10207  ackbij1lem14  10224  ackbij2lem2  10231  ackbij2lem3  10232  cf0  10242  cfeq0  10247  cfsuc  10248  cflim2  10254  isfin5  10290  isfin4p1  10306  fin1a2lem11  10401  fin1a2lem12  10402  fin1a2lem13  10403  axcc2lem  10427  ac6num  10470  zornn0g  10496  ttukeylem3  10502  brdom3  10519  iundom2g  10531  cardeq0  10543  pwcfsdom  10574  axpowndlem3  10590  canthwe  10642  canthp1lem1  10643  pwxpndom2  10656  pwdjundom  10658  gchxpidm  10660  intwun  10726  0tsk  10746  grothomex  10820  indpi  10898  fzennn  13929  hash0  14323  hashen1  14326  hashmap  14391  hashbc  14408  hashf1  14414  hashge3el3dif  14443  ccat1st1st  14574  swrdval  14589  swrd00  14590  swrd0  14604  cshfn  14736  cshnz  14738  0csh0  14739  incexclem  15778  incexc  15779  rexpen  16167  sadcf  16390  sadc0  16391  sadcp1  16392  smupf  16415  smup0  16416  smupp1  16417  0ram  16949  ram0  16951  cshws0  17031  str0  17118  ressbasOLD  17176  ress0  17184  0rest  17371  fnpr2ob  17500  xpsfrnel  17504  xpsle  17521  ismred2  17543  acsfn  17599  0cat  17629  ciclcl  17745  cicrcl  17746  cicer  17749  setcepi  18034  setc2obas  18040  setc2ohom  18041  cat1  18043  0pos  18270  0posOLD  18271  join0  18354  meet0  18355  mgm0b  18572  gsum0  18599  sgrp0b  18615  efmnd0nmnd  18767  pwmnd  18814  mulgfval  18946  ga0  19156  psgn0fv0  19373  pmtrsn  19381  oppglsm  19504  efgi0  19582  vrgpf  19630  vrgpinv  19631  frgpuptinv  19633  frgpup2  19638  0frgp  19641  frgpnabllem1  19735  frgpnabllem2  19736  dprd0  19895  dmdprdpr  19913  dprdpr  19914  00lsp  20584  cnfldfun  20948  frgpcyg  21120  frlmiscvec  21395  fvcoe1  21722  coe1f2  21724  coe1sfi  21728  coe1add  21777  coe1mul2lem1  21780  coe1mul2lem2  21781  coe1mul2  21782  ply1coe  21811  evls1rhmlem  21831  evl1sca  21844  evl1var  21846  pf1mpf  21862  pf1ind  21865  mat0dimscm  21962  mat0dimcrng  21963  mat0scmat  22031  mavmul0  22045  mavmul0g  22046  mvmumamul1  22047  mdet0pr  22085  mdet0f1o  22086  mdet0fv0  22087  mdetunilem9  22113  d0mat2pmat  22231  chpmat0d  22327  en1top  22478  en2top  22479  sn0topon  22492  indistopon  22495  indistps  22505  indistps2  22506  sn0cld  22585  indiscld  22586  neipeltop  22624  rest0  22664  restsn  22665  cmpfi  22903  refun0  23010  txindislem  23128  hmphindis  23292  xpstopnlem1  23304  xpstopnlem2  23306  ptcmpfi  23308  snfil  23359  fbasfip  23363  fgcl  23373  filconn  23378  fbasrn  23379  cfinfil  23388  csdfil  23389  supfil  23390  ufildr  23426  fin1aufil  23427  rnelfmlem  23447  fclsval  23503  tmdgsum  23590  tsmsfbas  23623  ust0  23715  ustn0  23716  0met  23863  xpsdsval  23878  minveclem3b  24936  tdeglem2  25570  deg1ldg  25601  deg1leb  25604  deg1val  25605  ulm0  25894  nosgnn0  27150  nodense  27184  nolt02o  27187  nogt01o  27188  nulsslt  27287  nulssgt  27288  bday1s  27321  made0  27357  precsexlem1  27642  precsexlem2  27643  uhgr0  28322  upgr0eop  28363  upgr0eopALT  28365  usgr0  28489  usgr0eop  28492  lfuhgr1v0e  28500  griedg0prc  28510  0grsubgr  28524  cplgr0  28671  0grrusgr  28825  clwwlk0on0  29334  0ewlk  29356  0wlkon  29362  0trlon  29366  0pthon  29369  0pthonv  29371  0conngr  29434  konigsberglem1  29494  konigsberglem2  29495  konigsberglem3  29496  wlkl0  29609  disjdifprg  31793  disjun0  31813  fpwrelmapffslem  31944  f1ocnt  32000  resvsca  32432  locfinref  32809  zarcmplem  32849  esumnul  33034  esumrnmpt2  33054  prsiga  33117  ldsysgenld  33146  ldgenpisyslem1  33149  oms0  33284  carsggect  33305  eulerpartgbij  33359  eulerpartlemmf  33362  repr0  33611  breprexp  33633  bnj941  33771  bnj97  33865  bnj149  33874  bnj150  33875  bnj944  33937  fineqvac  34085  derang0  34148  indispconn  34213  goeleq12bg  34328  satf0  34351  satf0op  34356  fmla0  34361  fmla0xp  34362  fmlasuc0  34363  fmlafvel  34364  fmlasuc  34365  fmlaomn0  34369  fmla0disjsuc  34377  satfdmfmla  34379  satfv0fvfmla0  34392  sate0  34394  sate0fv0  34396  sategoelfvb  34398  ex-sategoelel  34400  prv0  34409  prv1n  34410  rdgprc  34754  dfrdg3  34756  fullfunfnv  34906  fullfunfv  34907  rank0  35130  ssoninhaus  35321  onint1  35322  bj-0nel1  35822  bj-xpnzex  35828  bj-eltag  35846  bj-0eltag  35847  bj-tagss  35849  bj-pr1val  35873  bj-snex  35904  bj-snfromadj  35913  bj-nuliota  35926  bj-nuliotaALT  35927  bj-rdg0gALT  35940  bj-rest10  35957  bj-rest10b  35958  bj-rest0  35962  rdgssun  36247  finxpreclem1  36258  finxpreclem2  36259  finxp0  36260  finxpreclem5  36264  poimirlem28  36504  heibor1lem  36665  heiborlem6  36672  reheibor  36695  n0elqs  37183  sticksstones11  40960  mzpcompact2lem  41474  wopprc  41754  pw2f1ocnv  41761  pwslnmlem0  41818  pwfi2f1o  41823  2omomeqom  42038  cantnfub  42056  cantnfresb  42059  omcl3g  42069  nadd1suc  42127  naddwordnexlem4  42137  nla0002  42160  nla0003  42161  nla0001  42162  clsk1indlem0  42777  clsk1indlem4  42780  clsk1indlem1  42781  mnupwd  43011  mnuprdlem1  43016  mnuprdlem2  43017  mnuprdlem3  43018  mnurnd  43027  fnchoice  43698  eliuniincex  43783  limsup0  44396  0cnv  44444  liminf0  44495  0cnf  44579  dvnprodlem3  44650  qndenserrnbl  44997  prsal  45020  intsal  45032  sge00  45078  sge0sn  45081  nnfoctbdjlem  45157  isomenndlem  45232  hoiqssbl  45327  ovnsubadd2lem  45347  upwordnul  45580  iota0def  45734  aiota0def  45790  afv0fv0  45843  0nelsetpreimafv  46044  lincval0  47049  lco0  47061  linds0  47099  0aryfvalel  47273  0aryfvalelfv  47274  1aryenef  47284  2aryenef  47295  mof0  47457  0thinc  47624  setc2othin  47629  prstcthin  47649  bnd2d  47679