Theorem 0ex 5176

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

Syntax hints:  ¬ wn 3  ∀wal 1540   = wceq 1542  ∃wex 1786   ∈ wcel 2113  Vcvv 3398  ∅c0 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-nul 5175

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3847  df-nul 4213

This theorem is referenced by:  al0ssb  5177  sseliALT  5178  csbexg  5179  unisn2  5181  class2set  5221  0elpw  5223  0nep0  5225  unidif0  5227  iin0  5228  notzfaus  5229  notzfausOLD  5230  intv  5231  snexALT  5251  p0ex  5252  dtruALT  5256  zfpair  5289  snex  5299  dtruALT2  5303  opex  5323  opthwiener  5372  0sn0ep  5439  opthprc  5588  nrelv  5645  dmsnsnsn  6053  0elon  6226  nsuceq0  6253  snsn0non  6292  iotaex  6320  fun0  6405  fvrn0  6703  fvssunirn  6704  fprg  6928  ovima0  7344  onint0  7531  tfinds2  7598  finds  7630  finds2  7632  xpexr  7650  soex  7653  supp0  7862  fvn0elsupp  7876  fvn0elsuppb  7877  brtpos0  7929  reldmtpos  7930  tfrlem16  8059  tz7.44-1  8072  seqomlem1  8116  1n0  8151  el1o  8156  om0  8174  mapdm0  8453  fsetexb  8475  0map0sn0  8496  ixpexg  8533  0elixp  8540  en0  8619  en0OLD  8620  ensn1  8621  en1  8624  2dom  8630  map1  8640  xp1en  8653  endisj  8654  pw2eng  8673  map2xp  8738  limensuci  8744  1sdom  8801  unxpdom2  8806  sucxpdom  8807  isinf  8811  ac6sfi  8837  fodomfi  8871  0fsupp  8929  fi0  8958  oiexg  9073  brwdom  9105  brwdom2  9111  inf3lemb  9162  infeq5i  9173  dfom3  9184  cantnfvalf  9202  cantnfval2  9206  cantnfle  9208  cantnflt  9209  cantnff  9211  cantnf0  9212  cantnfp1lem1  9215  cantnfp1lem3  9217  cantnfp1  9218  cantnflem1a  9222  cantnflem1d  9225  cantnflem1  9226  cantnf  9230  cnfcomlem  9236  cnfcom  9237  cnfcom2lem  9238  cnfcom3  9241  tc0  9263  r10  9271  scottex  9388  djulcl  9413  djulf1o  9415  djuss  9423  djuun  9429  1stinl  9430  2ndinl  9431  infxpenlem  9514  fseqenlem1  9525  undjudom  9668  endjudisj  9669  djuen  9670  dju1dif  9673  dju1p1e2  9674  dju0en  9676  djucomen  9678  djuassen  9679  xpdjuen  9680  mapdjuen  9681  djuxpdom  9686  djuinf  9689  infdju1  9690  djulepw  9693  pwsdompw  9705  pwdjudom  9717  ackbij1lem14  9734  ackbij2lem2  9741  ackbij2lem3  9742  cf0  9752  cfeq0  9757  cfsuc  9758  cflim2  9764  isfin5  9800  isfin4p1  9816  fin1a2lem11  9911  fin1a2lem12  9912  fin1a2lem13  9913  axcc2lem  9937  ac6num  9980  zornn0g  10006  ttukeylem3  10012  brdom3  10029  iundom2g  10041  cardeq0  10053  pwcfsdom  10084  axpowndlem3  10100  canthwe  10152  canthp1lem1  10153  pwxpndom2  10166  pwdjundom  10168  gchxpidm  10170  intwun  10236  0tsk  10256  grothomex  10330  indpi  10408  fzennn  13428  hash0  13821  hashen1  13824  hashmap  13889  hashbc  13904  hashf1  13910  hashge3el3dif  13939  ccat1st1st  14074  swrdval  14095  swrd00  14096  swrd0  14110  cshfn  14242  cshnz  14244  0csh0  14245  incexclem  15285  incexc  15286  rexpen  15674  sadcf  15897  sadc0  15898  sadcp1  15899  smupf  15922  smup0  15923  smupp1  15924  0ram  16457  ram0  16459  cshws0  16539  str0  16639  ressbas  16658  ress0  16662  0rest  16807  fnpr2ob  16935  xpsfrnel  16939  xpsle  16956  ismred2  16978  acsfn  17034  0cat  17064  ciclcl  17178  cicrcl  17179  cicer  17182  setcepi  17461  setc2obas  17467  setc2ohom  17468  cat1  17470  0pos  17681  meet0  17864  join0  17865  mgm0b  17984  gsum0  18011  sgrp0b  18026  efmnd0nmnd  18172  pwmnd  18219  mulgfval  18345  ga0  18547  psgn0fv0  18758  pmtrsn  18766  oppglsm  18886  efgi0  18965  vrgpf  19013  vrgpinv  19014  frgpuptinv  19016  frgpup2  19021  0frgp  19024  frgpnabllem1  19113  frgpnabllem2  19114  dprd0  19273  dmdprdpr  19291  dprdpr  19292  00lsp  19873  cnfldfunALT  20231  frgpcyg  20393  frlmiscvec  20666  fvcoe1  20983  coe1f2  20985  coe1sfi  20989  coe1add  21040  coe1mul2lem1  21043  coe1mul2lem2  21044  coe1mul2  21045  ply1coe  21072  evls1rhmlem  21092  evl1sca  21105  evl1var  21107  pf1mpf  21123  pf1ind  21126  mat0dimscm  21221  mat0dimcrng  21222  mat0scmat  21290  mavmul0  21304  mavmul0g  21305  mvmumamul1  21306  mdet0pr  21344  mdet0f1o  21345  mdet0fv0  21346  mdetunilem9  21372  d0mat2pmat  21490  chpmat0d  21586  en1top  21736  en2top  21737  sn0topon  21750  indistopon  21753  indistps  21763  indistps2  21764  sn0cld  21842  indiscld  21843  neipeltop  21881  rest0  21921  restsn  21922  cmpfi  22160  refun0  22267  txindislem  22385  hmphindis  22549  xpstopnlem1  22561  xpstopnlem2  22563  ptcmpfi  22565  snfil  22616  fbasfip  22620  fgcl  22630  filconn  22635  fbasrn  22636  cfinfil  22645  csdfil  22646  supfil  22647  ufildr  22683  fin1aufil  22684  rnelfmlem  22704  fclsval  22760  tmdgsum  22847  tsmsfbas  22880  ust0  22972  ustn0  22973  0met  23120  xpsdsval  23135  minveclem3b  24181  tdeglem2  24814  deg1ldg  24845  deg1leb  24848  deg1val  24849  ulm0  25138  uhgr0  27018  upgr0eop  27059  upgr0eopALT  27061  usgr0  27185  usgr0eop  27188  lfuhgr1v0e  27196  griedg0prc  27206  0grsubgr  27220  cplgr0  27367  0grrusgr  27521  clwwlk0on0  28029  0ewlk  28051  0wlkon  28057  0trlon  28061  0pthon  28064  0pthonv  28066  0conngr  28129  konigsberglem1  28189  konigsberglem2  28190  konigsberglem3  28191  wlkl0  28304  disjdifprg  30488  disjun0  30508  fpwrelmapffslem  30642  f1ocnt  30698  resvsca  31106  locfinref  31363  zarcmplem  31403  esumnul  31586  esumrnmpt2  31606  prsiga  31669  ldsysgenld  31698  ldgenpisyslem1  31701  oms0  31834  carsggect  31855  eulerpartgbij  31909  eulerpartlemmf  31912  repr0  32161  breprexp  32183  bnj941  32323  bnj97  32417  bnj149  32426  bnj150  32427  bnj944  32489  fineqvac  32637  derang0  32702  indispconn  32767  goeleq12bg  32882  satf0  32905  satf0op  32910  fmla0  32915  fmla0xp  32916  fmlasuc0  32917  fmlafvel  32918  fmlasuc  32919  fmlaomn0  32923  fmla0disjsuc  32931  satfdmfmla  32933  satfv0fvfmla0  32946  sate0  32948  sate0fv0  32950  sategoelfvb  32952  ex-sategoelel  32954  prv0  32963  prv1n  32964  rdgprc  33342  dfrdg3  33344  trpredpred  33370  trpred0  33378  nosgnn0  33502  nodense  33536  nolt02o  33539  nogt01o  33540  nulsslt  33632  nulssgt  33633  bday1s  33666  made0  33695  fullfunfnv  33886  fullfunfv  33887  rank0  34110  ssoninhaus  34275  onint1  34276  bj-0nel1  34763  bj-xpnzex  34769  bj-eltag  34787  bj-0eltag  34788  bj-tagss  34790  bj-pr1val  34814  bj-nuliota  34848  bj-nuliotaALT  34849  bj-rest10  34877  bj-rest10b  34878  bj-rest0  34882  rdgssun  35169  finxpreclem1  35180  finxpreclem2  35181  finxp0  35182  finxpreclem5  35186  poimirlem28  35425  heibor1lem  35587  heiborlem6  35594  reheibor  35617  n0elqs  36081  mzpcompact2lem  40137  wopprc  40416  pw2f1ocnv  40423  pwslnmlem0  40480  pwfi2f1o  40485  clsk1indlem0  41189  clsk1indlem4  41192  clsk1indlem1  41193  mnupwd  41419  mnuprdlem1  41424  mnuprdlem2  41425  mnuprdlem3  41426  mnurnd  41435  fnchoice  42102  eliuniincex  42189  limsup0  42769  0cnv  42817  liminf0  42868  0cnf  42952  dvnprodlem3  43023  qndenserrnbl  43370  prsal  43393  intsal  43403  sge00  43448  sge0sn  43451  nnfoctbdjlem  43527  isomenndlem  43602  hoiqssbl  43697  ovnsubadd2lem  43717  iota0def  44063  aiota0def  44112  afv0fv0  44166  0nelsetpreimafv  44368  lincval0  45282  lco0  45294  linds0  45332  0aryfvalel  45506  0aryfvalelfv  45507  1aryenef  45517  2aryenef  45528  mof0  45687  0thinc  45788  setc2othin  45793  prstcthin  45806  bnd2d  45832