Theorem 0ex 5325

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

Syntax hints:  ¬ wn 3  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-nul 4353

This theorem is referenced by:  al0ssb  5326  sseliALT  5327  csbexg  5328  unisn2  5330  class2set  5373  0elpw  5374  0nep0  5376  unidif0  5378  iin0  5380  notzfaus  5381  intv  5382  snexALT  5401  p0ex  5402  dtruALT  5406  zfpair  5439  snex  5451  opex  5484  opthwiener  5533  0sn0ep  5603  opthprc  5764  nrelv  5824  dmsnsnsn  6251  0elon  6449  nsuceq0  6478  snsn0non  6520  iotaex  6546  iotaexOLD  6553  fun0  6643  fvrn0  6950  fvssunirnOLD  6954  fprg  7189  ovima0  7629  onint0  7827  tfinds2  7901  finds  7936  finds2  7938  xpexr  7958  soex  7961  supp0  8206  fvn0elsupp  8221  fvn0elsuppb  8222  brtpos0  8274  reldmtpos  8275  tfrlem16  8449  tz7.44-1  8462  seqomlem1  8506  1n0  8544  nlim1  8545  nlim2  8546  el1o  8551  om0  8573  mapdm0  8900  fsetexb  8922  0map0sn0  8943  ixpexg  8980  0elixp  8987  en0  9078  en0OLD  9079  en0ALT  9080  en0r  9081  ensn1  9082  ensn1OLD  9083  en1  9086  en1OLD  9087  2dom  9095  map1  9105  enpr2d  9115  xp1en  9123  endisj  9124  pw2eng  9144  0domg  9166  map2xp  9213  limensuci  9219  snnen2o  9300  0sdom1dom  9301  rex2dom  9309  1sdom2dom  9310  1sdomOLD  9312  unxpdom2  9317  sucxpdom  9318  isinf  9323  isinfOLD  9324  ac6sfi  9348  fodomfi  9378  fodomfiOLD  9398  0fsupp  9459  fi0  9489  oiexg  9604  brwdom  9636  brwdom2  9642  inf3lemb  9694  infeq5i  9705  dfom3  9716  cantnfvalf  9734  cantnfval2  9738  cantnfle  9740  cantnflt  9741  cantnff  9743  cantnf0  9744  cantnfp1lem1  9747  cantnfp1lem3  9749  cantnfp1  9750  cantnflem1a  9754  cantnflem1d  9757  cantnflem1  9758  cantnf  9762  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom3  9773  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  ttrclselem2  9795  tc0  9816  r10  9837  scottex  9954  djulcl  9979  djulf1o  9981  djuss  9989  djuun  9995  1stinl  9996  2ndinl  9997  infxpenlem  10082  fseqenlem1  10093  undjudom  10237  endjudisj  10238  djuen  10239  dju1dif  10242  dju1p1e2  10243  dju0en  10245  djucomen  10247  djuassen  10248  xpdjuen  10249  mapdjuen  10250  djuxpdom  10255  djuinf  10258  infdju1  10259  djulepw  10262  pwsdompw  10272  pwdjudom  10284  ackbij1lem14  10301  ackbij2lem2  10308  ackbij2lem3  10309  cf0  10320  cfeq0  10325  cfsuc  10326  cflim2  10332  isfin5  10368  isfin4p1  10384  fin1a2lem11  10479  fin1a2lem12  10480  fin1a2lem13  10481  axcc2lem  10505  ac6num  10548  zornn0g  10574  ttukeylem3  10580  brdom3  10597  iundom2g  10609  cardeq0  10621  pwcfsdom  10652  axpowndlem3  10668  canthwe  10720  canthp1lem1  10721  pwxpndom2  10734  pwdjundom  10736  gchxpidm  10738  intwun  10804  0tsk  10824  grothomex  10898  indpi  10976  fzennn  14019  hash0  14416  hashen1  14419  hashmap  14484  hashbc  14502  hashf1  14506  hashge3el3dif  14536  ccat1st1st  14676  swrdval  14691  swrd00  14692  swrd0  14706  cshfn  14838  cshnz  14840  0csh0  14841  incexclem  15884  incexc  15885  rexpen  16276  sadcf  16499  sadc0  16500  sadcp1  16501  smupf  16524  smup0  16525  smupp1  16526  0ram  17067  ram0  17069  cshws0  17149  str0  17236  ressbasOLD  17294  ress0  17302  0rest  17489  fnpr2ob  17618  xpsfrnel  17622  xpsle  17639  ismred2  17661  acsfn  17717  0cat  17747  ciclcl  17863  cicrcl  17864  cicer  17867  setcepi  18155  setc2obas  18161  setc2ohom  18162  cat1  18164  0pos  18391  0posOLD  18392  join0  18475  meet0  18476  mgm0b  18695  gsum0  18722  sgrp0b  18766  efmnd0nmnd  18925  pwmnd  18972  mulgfval  19109  ga0  19338  psgn0fv0  19553  pmtrsn  19561  oppglsm  19684  efgi0  19762  vrgpf  19810  vrgpinv  19811  frgpuptinv  19813  frgpup2  19818  0frgp  19821  frgpnabllem1  19915  frgpnabllem2  19916  dprd0  20075  dmdprdpr  20093  dprdpr  20094  00lsp  21002  cnfldfun  21401  cnfldfunOLD  21414  frgpcyg  21615  frlmiscvec  21892  fvcoe1  22230  coe1f2  22232  coe1sfi  22236  coe1add  22288  coe1mul2lem1  22291  coe1mul2lem2  22292  coe1mul2  22293  ply1coe  22323  evls1rhmlem  22346  evl1sca  22359  evl1var  22361  pf1mpf  22377  pf1ind  22380  mat0dimscm  22496  mat0dimcrng  22497  mat0scmat  22565  mavmul0  22579  mavmul0g  22580  mvmumamul1  22581  mdet0pr  22619  mdet0f1o  22620  mdet0fv0  22621  mdetunilem9  22647  d0mat2pmat  22765  chpmat0d  22861  en1top  23012  en2top  23013  sn0topon  23026  indistopon  23029  indistps  23039  indistps2  23040  sn0cld  23119  indiscld  23120  neipeltop  23158  rest0  23198  restsn  23199  cmpfi  23437  refun0  23544  txindislem  23662  hmphindis  23826  xpstopnlem1  23838  xpstopnlem2  23840  ptcmpfi  23842  snfil  23893  fbasfip  23897  fgcl  23907  filconn  23912  fbasrn  23913  cfinfil  23922  csdfil  23923  supfil  23924  ufildr  23960  fin1aufil  23961  rnelfmlem  23981  fclsval  24037  tmdgsum  24124  tsmsfbas  24157  ust0  24249  ustn0  24250  0met  24397  xpsdsval  24412  minveclem3b  25481  tdeglem2  26120  deg1ldg  26151  deg1leb  26154  deg1val  26155  ulm0  26452  nosgnn0  27721  nodense  27755  nolt02o  27758  nogt01o  27759  nulsslt  27860  nulssgt  27861  bday1s  27894  made0  27930  precsexlem1  28249  precsexlem2  28250  uhgr0  29108  upgr0eop  29149  upgr0eopALT  29151  usgr0  29278  usgr0eop  29281  lfuhgr1v0e  29289  griedg0prc  29299  0grsubgr  29313  cplgr0  29460  0grrusgr  29615  clwwlk0on0  30124  0ewlk  30146  0wlkon  30152  0trlon  30156  0pthon  30159  0pthonv  30161  0conngr  30224  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  wlkl0  30399  disjdifprg  32597  disjun0  32617  of0r  32696  fpwrelmapffslem  32746  f1ocnt  32807  resvsca  33321  1arithidom  33530  locfinref  33787  zarcmplem  33827  esumnul  34012  esumrnmpt2  34032  prsiga  34095  ldsysgenld  34124  ldgenpisyslem1  34127  oms0  34262  carsggect  34283  eulerpartgbij  34337  eulerpartlemmf  34340  repr0  34588  breprexp  34610  bnj941  34748  bnj97  34842  bnj149  34851  bnj150  34852  bnj944  34914  fineqvac  35073  wevgblacfn  35076  derang0  35137  indispconn  35202  goeleq12bg  35317  satf0  35340  satf0op  35345  fmla0  35350  fmla0xp  35351  fmlasuc0  35352  fmlafvel  35353  fmlasuc  35354  fmlaomn0  35358  fmla0disjsuc  35366  satfdmfmla  35368  satfv0fvfmla0  35381  sate0  35383  sate0fv0  35385  sategoelfvb  35387  ex-sategoelel  35389  prv0  35398  prv1n  35399  rdgprc  35758  dfrdg3  35760  fullfunfnv  35910  fullfunfv  35911  rank0  36134  ssoninhaus  36414  onint1  36415  bj-0nel1  36919  bj-xpnzex  36925  bj-eltag  36943  bj-0eltag  36944  bj-tagss  36946  bj-pr1val  36970  bj-snex  37001  bj-snfromadj  37010  bj-nuliota  37023  bj-nuliotaALT  37024  bj-rdg0gALT  37037  bj-rest10  37054  bj-rest10b  37055  bj-rest0  37059  rdgssun  37344  finxpreclem1  37355  finxpreclem2  37356  finxp0  37357  finxpreclem5  37361  poimirlem28  37608  heibor1lem  37769  heiborlem6  37776  reheibor  37799  n0elqs  38282  sticksstones11  42113  mzpcompact2lem  42707  wopprc  42987  pw2f1ocnv  42994  pwslnmlem0  43048  pwfi2f1o  43053  2omomeqom  43265  cantnfub  43283  cantnfresb  43286  omcl3g  43296  nadd1suc  43354  naddwordnexlem4  43363  nla0002  43386  nla0003  43387  nla0001  43388  clsk1indlem0  44003  clsk1indlem4  44006  clsk1indlem1  44007  mnupwd  44236  mnuprdlem1  44241  mnuprdlem2  44242  mnuprdlem3  44243  mnurnd  44252  fnchoice  44929  eliuniincex  45011  limsup0  45615  0cnv  45663  liminf0  45714  0cnf  45798  dvnprodlem3  45869  qndenserrnbl  46216  prsal  46239  intsal  46251  sge00  46297  sge0sn  46300  nnfoctbdjlem  46376  isomenndlem  46451  hoiqssbl  46546  ovnsubadd2lem  46566  upwordnul  46799  iota0def  46953  aiota0def  47011  afv0fv0  47064  0nelsetpreimafv  47264  lincval0  48144  lco0  48156  linds0  48194  0aryfvalel  48368  0aryfvalelfv  48369  1aryenef  48379  2aryenef  48390  mof0  48551  0thinc  48718  setc2othin  48723  prstcthin  48743  bnd2d  48773