Theorem 0ex 5249

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 5248. (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 5248	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4299	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3456	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3437  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-nul 4283

This theorem is referenced by:  al0ssb  5250  sseliALT  5251  csbexg  5252  unisn2  5254  class2set  5297  0elpw  5298  0nep0  5300  unidif0  5302  iin0  5304  notzfaus  5305  intv  5306  snexALT  5325  p0ex  5326  dtruALT  5330  zfpair  5363  snex  5378  opex  5409  opthwiener  5459  0sn0ep  5525  opthprc  5685  nrelv  5746  dmsnsnsn  6175  0elon  6369  nsuceq0  6399  snsn0non  6440  iotaex  6465  fun0  6554  fvrn0  6859  fprg  7097  ovima0  7534  onint0  7733  tfinds2  7803  finds  7835  finds2  7837  xpexr  7857  soex  7860  supp0  8104  fvn0elsupp  8119  fvn0elsuppb  8120  brtpos0  8172  reldmtpos  8173  tfrlem16  8321  tz7.44-1  8334  seqomlem1  8378  1n0  8412  nlim1  8413  nlim2  8414  el1o  8419  om0  8441  mapdm0  8775  fsetexb  8797  0map0sn0  8819  ixpexg  8856  0elixp  8863  en0  8951  en0ALT  8952  en0r  8953  ensn1  8954  en1  8957  2dom  8963  map1  8973  enpr2d  8981  xp1en  8987  endisj  8988  pw2eng  9007  0domg  9028  map2xp  9071  limensuci  9077  snnen2o  9140  0sdom1dom  9141  rex2dom  9148  1sdom2dom  9149  unxpdom2  9155  sucxpdom  9156  isinf  9160  ac6sfi  9179  fodomfi  9207  fodomfiOLD  9225  0fsupp  9285  fi0  9315  oiexg  9432  brwdom  9464  brwdom2  9470  inf3lemb  9526  infeq5i  9537  dfom3  9548  cantnfvalf  9566  cantnfval2  9570  cantnfle  9572  cantnflt  9573  cantnff  9575  cantnf0  9576  cantnfp1lem1  9579  cantnfp1lem3  9581  cantnfp1  9582  cantnflem1a  9586  cantnflem1d  9589  cantnflem1  9590  cantnf  9594  cnfcomlem  9600  cnfcom  9601  cnfcom2lem  9602  cnfcom3  9605  ssttrcl  9616  ttrcltr  9617  ttrclss  9621  dmttrcl  9622  ttrclselem2  9627  tc0  9646  r10  9672  scottex  9789  djulcl  9814  djulf1o  9816  djuss  9824  djuun  9830  1stinl  9831  2ndinl  9832  infxpenlem  9915  fseqenlem1  9926  undjudom  10070  endjudisj  10071  djuen  10072  dju1dif  10075  dju1p1e2  10076  dju0en  10078  djucomen  10080  djuassen  10081  xpdjuen  10082  mapdjuen  10083  djuxpdom  10088  djuinf  10091  infdju1  10092  djulepw  10095  pwsdompw  10105  pwdjudom  10117  ackbij1lem14  10134  ackbij2lem2  10141  ackbij2lem3  10142  cf0  10153  cfeq0  10158  cfsuc  10159  cflim2  10165  isfin5  10201  isfin4p1  10217  fin1a2lem11  10312  fin1a2lem12  10313  fin1a2lem13  10314  axcc2lem  10338  ac6num  10381  zornn0g  10407  ttukeylem3  10413  brdom3  10430  iundom2g  10442  cardeq0  10454  pwcfsdom  10485  axpowndlem3  10501  canthwe  10553  canthp1lem1  10554  pwxpndom2  10567  pwdjundom  10569  gchxpidm  10571  intwun  10637  0tsk  10657  grothomex  10731  indpi  10809  fzennn  13882  hash0  14281  hashen1  14284  hashmap  14349  hashbc  14367  hashf1  14371  hashge3el3dif  14401  ccat1st1st  14543  swrdval  14558  swrd00  14559  swrd0  14573  cshfn  14704  cshnz  14706  0csh0  14707  incexclem  15750  incexc  15751  rexpen  16144  sadcf  16371  sadc0  16372  sadcp1  16373  smupf  16396  smup0  16397  smupp1  16398  0ram  16939  ram0  16941  cshws0  17020  str0  17107  ress0  17161  0rest  17340  fnpr2ob  17470  xpsfrnel  17474  xpsle  17491  ismred2  17513  acsfn  17573  0cat  17603  ciclcl  17717  cicrcl  17718  cicer  17721  setcepi  18003  setc2obas  18009  setc2ohom  18010  cat1  18012  0pos  18235  join0  18317  meet0  18318  mgm0b  18573  gsum0  18600  sgrp0b  18644  efmnd0nmnd  18806  pwmnd  18853  mulgfval  18990  ga0  19218  psgn0fv0  19431  pmtrsn  19439  oppglsm  19562  efgi0  19640  vrgpf  19688  vrgpinv  19689  frgpuptinv  19691  frgpup2  19696  0frgp  19699  frgpnabllem1  19793  frgpnabllem2  19794  dprd0  19953  dmdprdpr  19971  dprdpr  19972  00lsp  20923  cnfldfun  21314  cnfldfunOLD  21327  frgpcyg  21519  frlmiscvec  21795  fvcoe1  22139  coe1f2  22141  coe1sfi  22145  coe1add  22197  coe1mul2lem1  22200  coe1mul2lem2  22201  coe1mul2  22202  ply1coe  22233  evls1rhmlem  22256  evl1sca  22269  evl1var  22271  pf1mpf  22287  pf1ind  22290  mat0dimscm  22404  mat0dimcrng  22405  mat0scmat  22473  mavmul0  22487  mavmul0g  22488  mvmumamul1  22489  mdet0pr  22527  mdet0f1o  22528  mdet0fv0  22529  mdetunilem9  22555  d0mat2pmat  22673  chpmat0d  22769  en1top  22919  en2top  22920  sn0topon  22933  indistopon  22936  indistps  22946  indistps2  22947  sn0cld  23025  indiscld  23026  neipeltop  23064  rest0  23104  restsn  23105  cmpfi  23343  refun0  23450  txindislem  23568  hmphindis  23732  xpstopnlem1  23744  xpstopnlem2  23746  ptcmpfi  23748  snfil  23799  fbasfip  23803  fgcl  23813  filconn  23818  fbasrn  23819  cfinfil  23828  csdfil  23829  supfil  23830  ufildr  23866  fin1aufil  23867  rnelfmlem  23887  fclsval  23943  tmdgsum  24030  tsmsfbas  24063  ust0  24155  ustn0  24156  0met  24301  xpsdsval  24316  minveclem3b  25375  tdeglem2  26013  deg1ldg  26044  deg1leb  26047  deg1val  26048  ulm0  26347  nosgnn0  27617  nodense  27651  nolt02o  27654  nogt01o  27655  nulsslt  27758  nulssgt  27759  bday1s  27795  made0  27838  precsexlem1  28165  precsexlem2  28166  uhgr0  29072  upgr0eop  29113  upgr0eopALT  29115  usgr0  29242  usgr0eop  29245  lfuhgr1v0e  29253  griedg0prc  29263  0grsubgr  29277  cplgr0  29424  0grrusgr  29579  clwwlk0on0  30093  0ewlk  30115  0wlkon  30121  0trlon  30125  0pthon  30128  0pthonv  30130  0conngr  30193  konigsberglem1  30253  konigsberglem2  30254  konigsberglem3  30255  wlkl0  30368  disjdifprg  32576  disjun0  32596  of0r  32684  fpwrelmapffslem  32739  f1ocnt  32808  resvsca  33341  1arithidom  33546  vieta  33664  locfinref  33926  zarcmplem  33966  esumnul  34133  esumrnmpt2  34153  prsiga  34216  ldsysgenld  34245  ldgenpisyslem1  34248  oms0  34382  carsggect  34403  eulerpartgbij  34457  eulerpartlemmf  34460  repr0  34696  breprexp  34718  bnj941  34856  bnj97  34950  bnj149  34959  bnj150  34960  bnj944  35022  fineqvac  35211  fineqvnttrclse  35216  wevgblacfn  35225  derang0  35285  indispconn  35350  goeleq12bg  35465  satf0  35488  satf0op  35493  fmla0  35498  fmla0xp  35499  fmlasuc0  35500  fmlafvel  35501  fmlasuc  35502  fmlaomn0  35506  fmla0disjsuc  35514  satfdmfmla  35516  satfv0fvfmla0  35529  sate0  35531  sate0fv0  35533  sategoelfvb  35535  ex-sategoelel  35537  prv0  35546  prv1n  35547  rdgprc  35908  dfrdg3  35910  fullfunfnv  36062  fullfunfv  36063  rank0  36286  ssoninhaus  36564  onint1  36565  bj-0nel1  37070  bj-xpnzex  37076  bj-eltag  37094  bj-0eltag  37095  bj-tagss  37097  bj-pr1val  37121  bj-snex  37152  bj-snfromadj  37161  bj-nuliota  37174  bj-nuliotaALT  37175  bj-rdg0gALT  37188  bj-rest10  37205  bj-rest10b  37206  bj-rest0  37210  rdgssun  37495  finxpreclem1  37506  finxpreclem2  37507  finxp0  37508  finxpreclem5  37512  poimirlem28  37761  heibor1lem  37922  heiborlem6  37929  reheibor  37952  n0elqs  38437  sticksstones11  42322  mzpcompact2lem  42908  wopprc  43187  pw2f1ocnv  43194  pwslnmlem0  43248  pwfi2f1o  43253  2omomeqom  43460  cantnfub  43478  cantnfresb  43481  omcl3g  43491  nadd1suc  43549  naddwordnexlem4  43558  nla0002  43581  nla0003  43582  nla0001  43583  clsk1indlem0  44198  clsk1indlem4  44201  clsk1indlem1  44202  mnupwd  44424  mnuprdlem1  44429  mnuprdlem2  44430  mnuprdlem3  44431  mnurnd  44440  permaxnul  45165  permaxinf2lem  45169  nregmodelf1o  45172  nregmodellem  45173  nregmodel  45174  fnchoice  45190  eliuniincex  45269  limsup0  45854  0cnv  45902  liminf0  45953  0cnf  46037  dvnprodlem3  46108  qndenserrnbl  46455  prsal  46478  intsal  46490  sge00  46536  sge0sn  46539  nnfoctbdjlem  46615  isomenndlem  46690  hoiqssbl  46785  ovnsubadd2lem  46805  iota0def  47200  aiota0def  47258  afv0fv0  47311  0nelsetpreimafv  47552  lincval0  48577  lco0  48589  linds0  48627  0aryfvalel  48796  0aryfvalelfv  48797  1aryenef  48807  2aryenef  48818  mof0  48999  dftpos5  49035  dftpos6  49036  relcic  49206  discsubclem  49224  discsubc  49225  iinfconstbas  49227  nelsubclem  49228  0funcg  49246  0func  49248  0funcALT  49249  oppffn  49285  oppfvalg  49287  fucofvalne  49486  0thinc  49620  setc2othin  49627  setc1ohomfval  49654  setc1ocofval  49655  isinito2lem  49659  prstcthin  49722  setc1onsubc  49763  initocmd  49830  termolmd  49831  bnd2d  49842