Theorem 0ex 5252

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

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

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 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-nul 4286

This theorem is referenced by:  al0ssb  5253  sseliALT  5254  csbexg  5255  unisn2  5257  class2set  5300  0elpw  5301  0nep0  5303  unidif0  5305  iin0  5307  notzfaus  5308  intv  5309  snexALT  5328  p0ex  5329  dtruALT  5333  zfpair  5366  snex  5381  opex  5412  opthwiener  5462  0sn0ep  5528  opthprc  5688  nrelv  5749  dmsnsnsn  6178  0elon  6372  nsuceq0  6402  snsn0non  6443  iotaex  6468  fun0  6557  fvrn0  6862  fprg  7100  ovima0  7537  onint0  7736  tfinds2  7806  finds  7838  finds2  7840  xpexr  7860  soex  7863  supp0  8107  fvn0elsupp  8122  fvn0elsuppb  8123  brtpos0  8175  reldmtpos  8176  tfrlem16  8324  tz7.44-1  8337  seqomlem1  8381  1n0  8415  nlim1  8416  nlim2  8417  el1o  8422  om0  8444  mapdm0  8779  fsetexb  8801  0map0sn0  8823  ixpexg  8860  0elixp  8867  en0  8955  en0ALT  8956  en0r  8957  ensn1  8958  en1  8961  2dom  8967  map1  8977  enpr2d  8985  xp1en  8991  endisj  8992  pw2eng  9011  0domg  9032  map2xp  9075  limensuci  9081  snnen2o  9145  0sdom1dom  9146  rex2dom  9153  1sdom2dom  9154  unxpdom2  9160  sucxpdom  9161  isinf  9165  ac6sfi  9184  fodomfi  9212  fodomfiOLD  9230  0fsupp  9293  fi0  9323  oiexg  9440  brwdom  9472  brwdom2  9478  inf3lemb  9534  infeq5i  9545  dfom3  9556  cantnfvalf  9574  cantnfval2  9578  cantnfle  9580  cantnflt  9581  cantnff  9583  cantnf0  9584  cantnfp1lem1  9587  cantnfp1lem3  9589  cantnfp1  9590  cantnflem1a  9594  cantnflem1d  9597  cantnflem1  9598  cantnf  9602  cnfcomlem  9608  cnfcom  9609  cnfcom2lem  9610  cnfcom3  9613  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  dmttrcl  9630  ttrclselem2  9635  tc0  9654  r10  9680  scottex  9797  djulcl  9822  djulf1o  9824  djuss  9832  djuun  9838  1stinl  9839  2ndinl  9840  infxpenlem  9923  fseqenlem1  9934  undjudom  10078  endjudisj  10079  djuen  10080  dju1dif  10083  dju1p1e2  10084  dju0en  10086  djucomen  10088  djuassen  10089  xpdjuen  10090  mapdjuen  10091  djuxpdom  10096  djuinf  10099  infdju1  10100  djulepw  10103  pwsdompw  10113  pwdjudom  10125  ackbij1lem14  10142  ackbij2lem2  10149  ackbij2lem3  10150  cf0  10161  cfeq0  10166  cfsuc  10167  cflim2  10173  isfin5  10209  isfin4p1  10225  fin1a2lem11  10320  fin1a2lem12  10321  fin1a2lem13  10322  axcc2lem  10346  ac6num  10389  zornn0g  10415  ttukeylem3  10421  brdom3  10438  iundom2g  10450  cardeq0  10462  pwcfsdom  10494  axpowndlem3  10510  canthwe  10562  canthp1lem1  10563  pwxpndom2  10576  pwdjundom  10578  gchxpidm  10580  intwun  10646  0tsk  10666  grothomex  10740  indpi  10818  fzennn  13891  hash0  14290  hashen1  14293  hashmap  14358  hashbc  14376  hashf1  14380  hashge3el3dif  14410  ccat1st1st  14552  swrdval  14567  swrd00  14568  swrd0  14582  cshfn  14713  cshnz  14715  0csh0  14716  incexclem  15759  incexc  15760  rexpen  16153  sadcf  16380  sadc0  16381  sadcp1  16382  smupf  16405  smup0  16406  smupp1  16407  0ram  16948  ram0  16950  cshws0  17029  str0  17116  ress0  17170  0rest  17349  fnpr2ob  17479  xpsfrnel  17483  xpsle  17500  ismred2  17522  acsfn  17582  0cat  17612  ciclcl  17726  cicrcl  17727  cicer  17730  setcepi  18012  setc2obas  18018  setc2ohom  18019  cat1  18021  0pos  18244  join0  18326  meet0  18327  mgm0b  18582  gsum0  18609  sgrp0b  18653  efmnd0nmnd  18815  pwmnd  18862  mulgfval  18999  ga0  19227  psgn0fv0  19440  pmtrsn  19448  oppglsm  19571  efgi0  19649  vrgpf  19697  vrgpinv  19698  frgpuptinv  19700  frgpup2  19705  0frgp  19708  frgpnabllem1  19802  frgpnabllem2  19803  dprd0  19962  dmdprdpr  19980  dprdpr  19981  00lsp  20932  cnfldfun  21323  cnfldfunOLD  21336  frgpcyg  21528  frlmiscvec  21804  fvcoe1  22148  coe1f2  22150  coe1sfi  22154  coe1add  22206  coe1mul2lem1  22209  coe1mul2lem2  22210  coe1mul2  22211  ply1coe  22242  evls1rhmlem  22265  evl1sca  22278  evl1var  22280  pf1mpf  22296  pf1ind  22299  mat0dimscm  22413  mat0dimcrng  22414  mat0scmat  22482  mavmul0  22496  mavmul0g  22497  mvmumamul1  22498  mdet0pr  22536  mdet0f1o  22537  mdet0fv0  22538  mdetunilem9  22564  d0mat2pmat  22682  chpmat0d  22778  en1top  22928  en2top  22929  sn0topon  22942  indistopon  22945  indistps  22955  indistps2  22956  sn0cld  23034  indiscld  23035  neipeltop  23073  rest0  23113  restsn  23114  cmpfi  23352  refun0  23459  txindislem  23577  hmphindis  23741  xpstopnlem1  23753  xpstopnlem2  23755  ptcmpfi  23757  snfil  23808  fbasfip  23812  fgcl  23822  filconn  23827  fbasrn  23828  cfinfil  23837  csdfil  23838  supfil  23839  ufildr  23875  fin1aufil  23876  rnelfmlem  23896  fclsval  23952  tmdgsum  24039  tsmsfbas  24072  ust0  24164  ustn0  24165  0met  24310  xpsdsval  24325  minveclem3b  25384  tdeglem2  26022  deg1ldg  26053  deg1leb  26056  deg1val  26057  ulm0  26356  nosgnn0  27626  nodense  27660  nolt02o  27663  nogt01o  27664  nulslts  27771  nulsgts  27772  bday1  27810  made0  27859  precsexlem1  28203  precsexlem2  28204  uhgr0  29146  upgr0eop  29187  upgr0eopALT  29189  usgr0  29316  usgr0eop  29319  lfuhgr1v0e  29327  griedg0prc  29337  0grsubgr  29351  cplgr0  29498  0grrusgr  29653  clwwlk0on0  30167  0ewlk  30189  0wlkon  30195  0trlon  30199  0pthon  30202  0pthonv  30204  0conngr  30267  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  wlkl0  30442  disjdifprg  32650  disjun0  32670  of0r  32758  fpwrelmapffslem  32811  f1ocnt  32880  resvsca  33413  1arithidom  33618  vieta  33736  locfinref  33998  zarcmplem  34038  esumnul  34205  esumrnmpt2  34225  prsiga  34288  ldsysgenld  34317  ldgenpisyslem1  34320  oms0  34454  carsggect  34475  eulerpartgbij  34529  eulerpartlemmf  34532  repr0  34768  breprexp  34790  bnj941  34928  bnj97  35022  bnj149  35031  bnj150  35032  bnj944  35094  fineqvac  35272  fineqvnttrclse  35280  wevgblacfn  35303  derang0  35363  indispconn  35428  goeleq12bg  35543  satf0  35566  satf0op  35571  fmla0  35576  fmla0xp  35577  fmlasuc0  35578  fmlafvel  35579  fmlasuc  35580  fmlaomn0  35584  fmla0disjsuc  35592  satfdmfmla  35594  satfv0fvfmla0  35607  sate0  35609  sate0fv0  35611  sategoelfvb  35613  ex-sategoelel  35615  prv0  35624  prv1n  35625  rdgprc  35986  dfrdg3  35988  fullfunfnv  36140  fullfunfv  36141  rank0  36364  ssoninhaus  36642  onint1  36643  bj-0nel1  37154  bj-xpnzex  37160  bj-eltag  37178  bj-0eltag  37179  bj-tagss  37181  bj-pr1val  37205  bj-snex  37236  bj-snfromadj  37245  bj-nuliota  37258  bj-nuliotaALT  37259  bj-rdg0gALT  37272  bj-rest10  37293  bj-rest10b  37294  bj-rest0  37298  rdgssun  37583  finxpreclem1  37594  finxpreclem2  37595  finxp0  37596  finxpreclem5  37600  poimirlem28  37849  heibor1lem  38010  heiborlem6  38017  reheibor  38040  n0elqs  38525  sticksstones11  42410  mzpcompact2lem  42993  wopprc  43272  pw2f1ocnv  43279  pwslnmlem0  43333  pwfi2f1o  43338  2omomeqom  43545  cantnfub  43563  cantnfresb  43566  omcl3g  43576  nadd1suc  43634  naddwordnexlem4  43643  nla0002  43665  nla0003  43666  nla0001  43667  clsk1indlem0  44282  clsk1indlem4  44285  clsk1indlem1  44286  mnupwd  44508  mnuprdlem1  44513  mnuprdlem2  44514  mnuprdlem3  44515  mnurnd  44524  permaxnul  45249  permaxinf2lem  45253  nregmodelf1o  45256  nregmodellem  45257  nregmodel  45258  fnchoice  45274  eliuniincex  45353  limsup0  45938  0cnv  45986  liminf0  46037  0cnf  46121  dvnprodlem3  46192  qndenserrnbl  46539  prsal  46562  intsal  46574  sge00  46620  sge0sn  46623  nnfoctbdjlem  46699  isomenndlem  46774  hoiqssbl  46869  ovnsubadd2lem  46889  iota0def  47284  aiota0def  47342  afv0fv0  47395  0nelsetpreimafv  47636  lincval0  48661  lco0  48673  linds0  48711  0aryfvalel  48880  0aryfvalelfv  48881  1aryenef  48891  2aryenef  48902  mof0  49083  dftpos5  49119  dftpos6  49120  relcic  49290  discsubclem  49308  discsubc  49309  iinfconstbas  49311  nelsubclem  49312  0funcg  49330  0func  49332  0funcALT  49333  oppffn  49369  oppfvalg  49371  fucofvalne  49570  0thinc  49704  setc2othin  49711  setc1ohomfval  49738  setc1ocofval  49739  isinito2lem  49743  prstcthin  49806  setc1onsubc  49847  initocmd  49914  termolmd  49915  bnd2d  49926