Theorem 0ex 5298

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

Syntax hints:  ¬ wn 3  ∀wal 1531   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3466  ∅c0 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5297

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3944  df-nul 4316

This theorem is referenced by:  al0ssb  5299  sseliALT  5300  csbexg  5301  unisn2  5303  class2set  5344  0elpw  5345  0nep0  5347  unidif0  5349  iin0  5351  notzfaus  5352  intv  5353  snexALT  5372  p0ex  5373  dtruALT  5377  zfpair  5410  snex  5422  opex  5455  opthwiener  5505  0sn0ep  5575  opthprc  5731  nrelv  5791  dmsnsnsn  6210  0elon  6409  nsuceq0  6438  snsn0non  6480  iotaex  6507  iotaexOLD  6514  fun0  6604  fvrn0  6912  fvssunirnOLD  6916  fprg  7146  ovima0  7580  onint0  7773  tfinds2  7847  finds  7883  finds2  7885  xpexr  7903  soex  7906  supp0  8146  fvn0elsupp  8160  fvn0elsuppb  8161  brtpos0  8214  reldmtpos  8215  tfrlem16  8389  tz7.44-1  8402  seqomlem1  8446  1n0  8484  nlim1  8485  nlim2  8486  el1o  8491  om0  8513  mapdm0  8833  fsetexb  8855  0map0sn0  8876  ixpexg  8913  0elixp  8920  en0  9010  en0OLD  9011  en0ALT  9012  en0r  9013  ensn1  9014  ensn1OLD  9015  en1  9018  en1OLD  9019  2dom  9027  map1  9037  enpr2d  9046  xp1en  9054  endisj  9055  pw2eng  9075  0domg  9097  map2xp  9144  limensuci  9150  snnen2o  9234  0sdom1dom  9235  rex2dom  9243  1sdom2dom  9244  1sdomOLD  9246  unxpdom2  9251  sucxpdom  9252  isinf  9257  isinfOLD  9258  ac6sfi  9284  fodomfi  9322  0fsupp  9382  fi0  9412  oiexg  9527  brwdom  9559  brwdom2  9565  inf3lemb  9617  infeq5i  9628  dfom3  9639  cantnfvalf  9657  cantnfval2  9661  cantnfle  9663  cantnflt  9664  cantnff  9666  cantnf0  9667  cantnfp1lem1  9670  cantnfp1lem3  9672  cantnfp1  9673  cantnflem1a  9677  cantnflem1d  9680  cantnflem1  9681  cantnf  9685  cnfcomlem  9691  cnfcom  9692  cnfcom2lem  9693  cnfcom3  9696  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  dmttrcl  9713  ttrclselem2  9718  tc0  9739  r10  9760  scottex  9877  djulcl  9902  djulf1o  9904  djuss  9912  djuun  9918  1stinl  9919  2ndinl  9920  infxpenlem  10005  fseqenlem1  10016  undjudom  10159  endjudisj  10160  djuen  10161  dju1dif  10164  dju1p1e2  10165  dju0en  10167  djucomen  10169  djuassen  10170  xpdjuen  10171  mapdjuen  10172  djuxpdom  10177  djuinf  10180  infdju1  10181  djulepw  10184  pwsdompw  10196  pwdjudom  10208  ackbij1lem14  10225  ackbij2lem2  10232  ackbij2lem3  10233  cf0  10243  cfeq0  10248  cfsuc  10249  cflim2  10255  isfin5  10291  isfin4p1  10307  fin1a2lem11  10402  fin1a2lem12  10403  fin1a2lem13  10404  axcc2lem  10428  ac6num  10471  zornn0g  10497  ttukeylem3  10503  brdom3  10520  iundom2g  10532  cardeq0  10544  pwcfsdom  10575  axpowndlem3  10591  canthwe  10643  canthp1lem1  10644  pwxpndom2  10657  pwdjundom  10659  gchxpidm  10661  intwun  10727  0tsk  10747  grothomex  10821  indpi  10899  fzennn  13931  hash0  14325  hashen1  14328  hashmap  14393  hashbc  14410  hashf1  14416  hashge3el3dif  14445  ccat1st1st  14576  swrdval  14591  swrd00  14592  swrd0  14606  cshfn  14738  cshnz  14740  0csh0  14741  incexclem  15780  incexc  15781  rexpen  16170  sadcf  16393  sadc0  16394  sadcp1  16395  smupf  16418  smup0  16419  smupp1  16420  0ram  16954  ram0  16956  cshws0  17036  str0  17123  ressbasOLD  17181  ress0  17189  0rest  17376  fnpr2ob  17505  xpsfrnel  17509  xpsle  17526  ismred2  17548  acsfn  17604  0cat  17634  ciclcl  17750  cicrcl  17751  cicer  17754  setcepi  18042  setc2obas  18048  setc2ohom  18049  cat1  18051  0pos  18278  0posOLD  18279  join0  18362  meet0  18363  mgm0b  18582  gsum0  18609  sgrp0b  18653  efmnd0nmnd  18807  pwmnd  18854  mulgfval  18989  ga0  19206  psgn0fv0  19423  pmtrsn  19431  oppglsm  19554  efgi0  19632  vrgpf  19680  vrgpinv  19681  frgpuptinv  19683  frgpup2  19688  0frgp  19691  frgpnabllem1  19785  frgpnabllem2  19786  dprd0  19945  dmdprdpr  19963  dprdpr  19964  00lsp  20820  cnfldfun  21242  frgpcyg  21438  frlmiscvec  21714  fvcoe1  22051  coe1f2  22053  coe1sfi  22057  coe1add  22107  coe1mul2lem1  22110  coe1mul2lem2  22111  coe1mul2  22112  ply1coe  22141  evls1rhmlem  22164  evl1sca  22177  evl1var  22179  pf1mpf  22195  pf1ind  22198  mat0dimscm  22295  mat0dimcrng  22296  mat0scmat  22364  mavmul0  22378  mavmul0g  22379  mvmumamul1  22380  mdet0pr  22418  mdet0f1o  22419  mdet0fv0  22420  mdetunilem9  22446  d0mat2pmat  22564  chpmat0d  22660  en1top  22811  en2top  22812  sn0topon  22825  indistopon  22828  indistps  22838  indistps2  22839  sn0cld  22918  indiscld  22919  neipeltop  22957  rest0  22997  restsn  22998  cmpfi  23236  refun0  23343  txindislem  23461  hmphindis  23625  xpstopnlem1  23637  xpstopnlem2  23639  ptcmpfi  23641  snfil  23692  fbasfip  23696  fgcl  23706  filconn  23711  fbasrn  23712  cfinfil  23721  csdfil  23722  supfil  23723  ufildr  23759  fin1aufil  23760  rnelfmlem  23780  fclsval  23836  tmdgsum  23923  tsmsfbas  23956  ust0  24048  ustn0  24049  0met  24196  xpsdsval  24211  minveclem3b  25280  tdeglem2  25921  deg1ldg  25952  deg1leb  25955  deg1val  25956  ulm0  26246  nosgnn0  27510  nodense  27544  nolt02o  27547  nogt01o  27548  nulsslt  27649  nulssgt  27650  bday1s  27683  made0  27719  precsexlem1  28024  precsexlem2  28025  uhgr0  28805  upgr0eop  28846  upgr0eopALT  28848  usgr0  28972  usgr0eop  28975  lfuhgr1v0e  28983  griedg0prc  28993  0grsubgr  29007  cplgr0  29154  0grrusgr  29308  clwwlk0on0  29817  0ewlk  29839  0wlkon  29845  0trlon  29849  0pthon  29852  0pthonv  29854  0conngr  29917  konigsberglem1  29977  konigsberglem2  29978  konigsberglem3  29979  wlkl0  30092  disjdifprg  32278  disjun0  32298  fpwrelmapffslem  32429  f1ocnt  32485  resvsca  32913  locfinref  33313  zarcmplem  33353  esumnul  33538  esumrnmpt2  33558  prsiga  33621  ldsysgenld  33650  ldgenpisyslem1  33653  oms0  33788  carsggect  33809  eulerpartgbij  33863  eulerpartlemmf  33866  repr0  34114  breprexp  34136  bnj941  34274  bnj97  34368  bnj149  34377  bnj150  34378  bnj944  34440  fineqvac  34588  derang0  34651  indispconn  34716  goeleq12bg  34831  satf0  34854  satf0op  34859  fmla0  34864  fmla0xp  34865  fmlasuc0  34866  fmlafvel  34867  fmlasuc  34868  fmlaomn0  34872  fmla0disjsuc  34880  satfdmfmla  34882  satfv0fvfmla0  34895  sate0  34897  sate0fv0  34899  sategoelfvb  34901  ex-sategoelel  34903  prv0  34912  prv1n  34913  rdgprc  35262  dfrdg3  35264  fullfunfnv  35414  fullfunfv  35415  rank0  35638  gg-cnfldfun  35671  ssoninhaus  35824  onint1  35825  bj-0nel1  36325  bj-xpnzex  36331  bj-eltag  36349  bj-0eltag  36350  bj-tagss  36352  bj-pr1val  36376  bj-snex  36407  bj-snfromadj  36416  bj-nuliota  36429  bj-nuliotaALT  36430  bj-rdg0gALT  36443  bj-rest10  36460  bj-rest10b  36461  bj-rest0  36465  rdgssun  36750  finxpreclem1  36761  finxpreclem2  36762  finxp0  36763  finxpreclem5  36767  poimirlem28  37010  heibor1lem  37171  heiborlem6  37178  reheibor  37201  n0elqs  37689  sticksstones11  41469  mzpcompact2lem  42003  wopprc  42283  pw2f1ocnv  42290  pwslnmlem0  42347  pwfi2f1o  42352  2omomeqom  42567  cantnfub  42585  cantnfresb  42588  omcl3g  42598  nadd1suc  42656  naddwordnexlem4  42666  nla0002  42689  nla0003  42690  nla0001  42691  clsk1indlem0  43306  clsk1indlem4  43309  clsk1indlem1  43310  mnupwd  43540  mnuprdlem1  43545  mnuprdlem2  43546  mnuprdlem3  43547  mnurnd  43556  fnchoice  44227  eliuniincex  44311  limsup0  44920  0cnv  44968  liminf0  45019  0cnf  45103  dvnprodlem3  45174  qndenserrnbl  45521  prsal  45544  intsal  45556  sge00  45602  sge0sn  45605  nnfoctbdjlem  45681  isomenndlem  45756  hoiqssbl  45851  ovnsubadd2lem  45871  upwordnul  46104  iota0def  46258  aiota0def  46314  afv0fv0  46367  0nelsetpreimafv  46568  lincval0  47309  lco0  47321  linds0  47359  0aryfvalel  47533  0aryfvalelfv  47534  1aryenef  47544  2aryenef  47555  mof0  47716  0thinc  47883  setc2othin  47888  prstcthin  47908  bnd2d  47938