Theorem 0ex 5264

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 5263. (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 5263	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4297	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3469	1 ⊢ ∅ ∈ V

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-nul 4280

This theorem is used by:  al0ssb  5265  sseliALT  5266  csbexg  5267  unisn2  5269  class2set  5319  0elpw  5320  0nep0  5322  unidif0  5324  unidif0OLD  5325  iin0  5327  notsep  5328  intv  5329  snexALT  5348  p0ex  5349  dtruALT  5353  zfpair  5386  snexOLD  5407  opexOLD  5440  opthwiener  5491  0sn0ep  5559  opthprc  5719  nrelv  5780  nrelvOLD  5781  dmsnsnsn  6216  0elon  6413  nsuceq0  6443  snsn0non  6484  iotaex  6509  fun0  6598  fvrn0  6906  fprg  7152  ovima0  7593  onint0  7790  tfinds2  7860  finds  7893  finds2  7895  xpexr  7915  soex  7918  supp0  8163  fvn0elsupp  8178  fvn0elsuppb  8179  brtpos0  8231  reldmtpos  8232  tfrlem16  8382  tz7.44-1  8395  seqomlem1  8439  1n0OLD  8475  nlim1  8476  nlim2  8477  el1o  8482  om0  8504  mapdm0  8841  fsetexb  8865  0map0sn0  8892  ixpexg  8929  0elixp  8936  en0  9024  en0ALT  9025  en0r  9026  ensn1  9027  en1  9030  2dom  9037  map1  9047  enpr2d  9055  xp1en  9061  endisj  9062  pw2eng  9081  0domg  9102  map2xp  9145  limensuci  9151  snnen2o  9215  0sdom1dom  9216  rex2dom  9223  1sdom2dom  9224  unxpdom2  9230  sucxpdom  9231  isinf  9235  ac6sfi  9254  fodomfi  9282  0fsupp  9360  fi0  9390  oiexg  9507  brwdom  9539  brwdom2  9545  inf3lemb  9604  infeq5i  9615  dfom3  9626  cantnfvalf  9644  cantnfval2  9648  cantnfle  9650  cantnflt  9651  cantnff  9653  cantnf0  9654  cantnfp1lem1  9657  cantnfp1lem3  9659  cantnfp1  9660  cantnflem1a  9664  cantnflem1d  9667  cantnflem1  9668  cantnf  9672  cnfcomlem  9678  cnfcom  9679  cnfcom2lem  9680  cnfcom3  9683  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  dmttrcl  9700  ttrclselem2  9705  tc0  9724  r10  9750  scottex  9872  scottexOLD  9873  djulcl  9915  djulf1o  9917  djuss  9925  djuun  9931  1stinl  9932  2ndinl  9933  infxpenlem  10016  fseqenlem1  10027  undjudom  10170  endjudisj  10171  djuen  10172  dju1dif  10175  dju1p1e2  10176  dju0en  10178  djucomen  10180  djuassen  10181  xpdjuen  10182  mapdjuen  10183  djuxpdom  10188  djuinf  10191  infdju1  10192  djulepw  10195  pwsdompw  10205  pwdjudom  10217  ackbij1lem14  10234  ackbij2lem2  10241  ackbij2lem3  10242  cf0  10252  cfeq0  10258  cfsuc  10259  cflim2  10265  isfin5  10301  isfin4p1  10317  fin1a2lem11  10412  fin1a2lem12  10413  fin1a2lem13  10414  axcc2lem  10438  ac6num  10481  zornn0g  10507  ttukeylem3  10513  brdom3  10531  iundom2g  10548  cardeq0  10560  pwcfsdom  10592  axpowndlem3  10608  canthwe  10660  canthp1lem1  10661  pwxpndom2  10674  pwdjundom  10676  gchxpidm  10678  intwun  10744  0tsk  10764  grothomex  10838  indpi  10916  fzennn  14032  hash0  14431  hashen1  14434  hashmap  14500  hashbc  14518  hashf1  14522  hashge3el3dif  14552  ccat1st1st  14696  swrdval  14711  swrd00  14712  swrd0  14728  cshfn  14861  cshnz  14863  0csh0  14864  incexclem  15925  incexc  15926  rexpen  16316  sadcf  16543  sadc0  16544  sadcp1  16545  smupf  16568  smup0  16569  smupp1  16570  0ram  17112  ram0  17114  cshws0  17193  str0  17281  ress0  17335  0rest  17514  fnpr2ob  17644  xpsfrnel  17648  xpsle  17665  ismred2  17687  acsfn  17747  0cat  17777  ciclcl  17891  cicrcl  17892  cicer  17895  setcepi  18177  setc2obas  18183  setc2ohom  18184  cat1  18186  0pos  18409  join0  18491  meet0  18492  mgm0b  18749  gsum0  18786  sgrp0b  18830  efmnd0nmnd  18999  degenmgmopdm  19047  degenmgmnfn  19049  degenmgm  19050  degenmgm2  19053  pwmnd  19056  mulgfval  19192  ga0  19425  psgn0fv0  19638  pmtrsn  19646  oppglsm  19769  efgi0  19847  vrgpf  19895  vrgpinv  19896  frgpuptinv  19898  frgpup2  19903  0frgp  19906  frgpnabllem1  20000  frgpnabllem2  20001  dprd0  20160  dmdprdpr  20178  dprdpr  20179  00lsp  21165  cnfldfun  21599  frgpcyg  21786  frlmiscvec  22062  fvcoe1  22432  coe1f2  22434  coe1sfi  22438  coe1add  22490  coe1mul2lem1  22493  coe1mul2lem2  22494  coe1mul2  22495  ply1coe  22523  evls1rhmlem  22546  evl1sca  22559  evl1var  22561  pf1mpf  22577  pf1ind  22580  mat0dimscm  22691  mat0dimcrng  22692  mat0scmat  22760  mavmul0  22774  mavmul0g  22775  mvmumamul1  22776  mdet0pr  22814  mdet0f1o  22815  mdet0fv0  22816  mdetunilem9  22842  d0mat2pmat  22963  chpmat0d  23059  en1top  23209  en2top  23210  sn0topon  23223  indistopon  23226  indistps  23236  indistps2  23237  sn0cld  23315  indiscld  23316  neipeltop  23354  rest0  23394  restsn  23395  cmpfi  23633  refun0  23741  txindislem  23859  hmphindis  24023  xpstopnlem1  24035  xpstopnlem2  24037  ptcmpfi  24039  snfil  24090  fbasfip  24094  fgcl  24104  filconn  24109  fbasrn  24110  cfinfil  24119  csdfil  24120  supfil  24121  ufildr  24157  fin1aufil  24158  rnelfmlem  24178  fclsval  24234  tmdgsum  24321  tsmsfbas  24354  ust0  24446  ustn0  24447  0met  24592  xpsdsval  24607  minveclem3b  25656  tdeglem2  26286  deg1ldg  26317  deg1leb  26320  deg1val  26321  ulm0  26627  nosgnn0  27894  nodense  27928  nolt02o  27931  nogt01o  27932  nulslts  28040  nulsgts  28041  bday1  28079  made0  28128  precsexlem1  28472  precsexlem2  28473  uhgr0  29530  upgr0eop  29571  upgr0eopALT  29573  usgr0  29703  usgr0eop  29706  lfuhgr1v0e  29714  griedg0prc  29724  0grsubgr  29738  cplgr0  29885  0grrusgr  30039  clwwlk0on0  30562  0ewlk  30584  0wlkon  30590  0trlon  30594  0pthon  30597  0pthonv  30599  0conngr  30672  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  wlkl0  30847  disjdifprg  33048  disjun0  33068  of0r  33152  fpwrelmapffslem  33203  f1ocnt  33271  resvsca  33772  1arithidom  33947  0mplrim  34024  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhm0  34036  mplidomlem  34037  vieta  34090  locfinref  34351  zarcmplem  34391  esumnul  34558  esumrnmpt2  34578  prsiga  34641  ldsysgenld  34671  ldgenpisyslem1  34674  oms0  34808  carsggect  34829  eulerpartgbij  34883  eulerpartlemmf  34886  repr0  35119  breprexp  35141  bnj941  35282  bnj97  35375  bnj149  35384  bnj150  35385  bnj944  35447  fineqvac  35642  fineqvnttrclse  35650  kard0  35680  kard0b  35685  wevgblacfn  35708  derang0  35748  indispconn  35813  goeleq12bg  35928  satf0  35951  satf0op  35956  fmla0  35961  fmla0xp  35962  fmlasuc0  35963  fmlafvel  35964  fmlasuc  35965  fmlaomn0  35969  fmla0disjsuc  35977  satfdmfmla  35979  satfv0fvfmla0  35992  sate0  35994  sate0fv0  35996  sategoelfvb  35998  ex-sategoelel  36000  prv0  36009  prv1n  36010  rdgprc  36371  dfrdg3  36373  fullfunfnv  36525  fullfunfv  36526  rank0  36750  nmulrid  36777  ssoninhaus  37067  onint1  37068  mh-infprim2bi  37166  bj-0nel1  37697  bj-xpnzex  37703  bj-eltag  37721  bj-0eltag  37722  bj-tagss  37724  bj-pr1val  37748  bj-snex  37779  bj-snfromadj  37788  bj-nuliota  37801  bj-nuliotaALT  37802  bj-rdg0gALT  37815  bj-rest10  37838  bj-rest10b  37839  bj-rest0  37843  rdgssun  38132  finxpreclem1  38143  finxpreclem2  38144  finxp0  38145  finxpreclem5  38149  poimirlem28  38397  heibor1lem  38559  heiborlem6  38566  reheibor  38589  n0elqs  39080  sticksstones11  43022  mzpcompact2lem  43596  wopprc  43871  pw2f1ocnv  43878  pwslnmlem0  43932  pwfi2f1o  43937  2omomeqom  44144  cantnfub  44162  cantnfresb  44165  omcl3g  44175  nadd1suc  44233  naddwordnexlem4  44242  nla0002  44264  nla0003  44265  nla0001  44266  clsk1indlem0  44881  clsk1indlem4  44884  clsk1indlem1  44885  mnupwd  45091  mnuprdlem1  45096  mnuprdlem2  45097  mnuprdlem3  45098  mnurnd  45107  permaxnul  45831  permaxinf2lem  45835  nregmodelf1o  45838  nregmodellem  45839  nregmodel  45840  fnchoice  45863  eliuniincex  45941  limsup0  46522  0cnv  46570  liminf0  46621  0cnf  46705  dvnprodlem3  46776  qndenserrnbl  47123  prsal  47146  intsal  47158  sge00  47204  sge0sn  47207  nnfoctbdjlem  47283  isomenndlem  47358  hoiqssbl  47453  ovnsubadd2lem  47473  iota0def  47926  aiota0def  47984  afv0fv0  48037  0nelsetpreimafv  48290  lincval0  49345  lco0  49357  linds0  49395  0aryfvalel  49564  0aryfvalelfv  49565  1aryenef  49575  2aryenef  49586  mof0  49766  dftpos5  49800  dftpos6  49801  relcic  49971  discsubclem  49989  discsubc  49990  iinfconstbas  49992  nelsubclem  49993  0funcg  50011  0func  50013  0funcALT  50014  oppffn  50050  oppfvalg  50052  fucofvalne  50251  0thinc  50385  setc2othin  50392  setc1ohomfval  50419  setc1ocofval  50420  isinito2lem  50424  prstcthin  50487  setc1onsubc  50528  initocmd  50595  termolmd  50596  bnd2d  50607