Theorem 0ex 5175

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

Syntax hints:  ¬ wn 3  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-nul 4244

This theorem is referenced by:  al0ssb  5176  sseliALT  5177  csbexg  5178  unisn2  5180  class2set  5219  0elpw  5221  0nep0  5223  unidif0  5225  iin0  5226  notzfaus  5227  notzfausOLD  5228  intv  5229  snexALT  5249  p0ex  5250  dtruALT  5254  zfpair  5287  snex  5297  dtruALT2  5301  opex  5321  opthwiener  5369  0sn0ep  5434  opthprc  5580  nrelv  5637  dmsnsnsn  6044  0elon  6212  nsuceq0  6239  snsn0non  6277  iotaex  6304  fun0  6389  fvrn0  6673  fvssunirn  6674  fprg  6894  ovima0  7307  onint0  7491  tfinds2  7558  finds  7589  finds2  7591  xpexr  7605  soex  7608  supp0  7818  fvn0elsupp  7829  fvn0elsuppb  7830  brtpos0  7882  reldmtpos  7883  tfrlem16  8012  tz7.44-1  8025  seqomlem1  8069  1n0  8102  el1o  8107  om0  8125  mapdm0  8404  0map0sn0  8432  ixpexg  8469  0elixp  8476  en0  8555  ensn1  8556  en1  8559  2dom  8565  map1  8575  xp1en  8586  endisj  8587  pw2eng  8606  map2xp  8671  limensuci  8677  1sdom  8705  unxpdom2  8710  sucxpdom  8711  isinf  8715  ac6sfi  8746  fodomfi  8781  0fsupp  8839  fi0  8868  oiexg  8983  brwdom  9015  brwdom2  9021  inf3lemb  9072  infeq5i  9083  dfom3  9094  cantnfvalf  9112  cantnfval2  9116  cantnfle  9118  cantnflt  9119  cantnff  9121  cantnf0  9122  cantnfp1lem1  9125  cantnfp1lem3  9127  cantnfp1  9128  cantnflem1a  9132  cantnflem1d  9135  cantnflem1  9136  cantnf  9140  cnfcomlem  9146  cnfcom  9147  cnfcom2lem  9148  cnfcom3  9151  tc0  9173  r10  9181  scottex  9298  djulcl  9323  djulf1o  9325  djuss  9333  djuun  9339  1stinl  9340  2ndinl  9341  infxpenlem  9424  fseqenlem1  9435  undjudom  9578  endjudisj  9579  djuen  9580  dju1dif  9583  dju1p1e2  9584  dju0en  9586  djucomen  9588  djuassen  9589  xpdjuen  9590  mapdjuen  9591  djuxpdom  9596  djuinf  9599  infdju1  9600  djulepw  9603  pwsdompw  9615  pwdjudom  9627  ackbij1lem14  9644  ackbij2lem2  9651  ackbij2lem3  9652  cf0  9662  cfeq0  9667  cfsuc  9668  cflim2  9674  isfin5  9710  isfin4p1  9726  fin1a2lem11  9821  fin1a2lem12  9822  fin1a2lem13  9823  axcc2lem  9847  ac6num  9890  zornn0g  9916  ttukeylem3  9922  brdom3  9939  iundom2g  9951  cardeq0  9963  pwcfsdom  9994  axpowndlem3  10010  canthwe  10062  canthp1lem1  10063  pwxpndom2  10076  pwdjundom  10078  gchxpidm  10080  intwun  10146  0tsk  10166  grothomex  10240  indpi  10318  fzennn  13331  hash0  13724  hashen1  13727  hashmap  13792  hashbc  13807  hashf1  13811  hashge3el3dif  13840  ccat1st1st  13975  swrdval  13996  swrd00  13997  swrd0  14011  cshfn  14143  cshnz  14145  0csh0  14146  incexclem  15183  incexc  15184  rexpen  15573  sadcf  15792  sadc0  15793  sadcp1  15794  smupf  15817  smup0  15818  smupp1  15819  0ram  16346  ram0  16348  cshws0  16427  str0  16527  ressbas  16546  ress0  16550  0rest  16695  fnpr2ob  16823  xpsfrnel  16827  xpsle  16844  ismred2  16866  acsfn  16922  0cat  16951  ciclcl  17064  cicrcl  17065  cicer  17068  setcepi  17340  0pos  17556  meet0  17739  join0  17740  mgm0b  17859  gsum0  17886  sgrp0b  17901  efmnd0nmnd  18047  pwmnd  18094  mulgfval  18218  ga0  18420  psgn0fv0  18631  pmtrsn  18639  oppglsm  18759  efgi0  18838  vrgpf  18886  vrgpinv  18887  frgpuptinv  18889  frgpup2  18894  0frgp  18897  frgpnabllem1  18986  frgpnabllem2  18987  dprd0  19146  dmdprdpr  19164  dprdpr  19165  00lsp  19746  cnfldfunALT  20104  frgpcyg  20265  frlmiscvec  20538  fvcoe1  20836  coe1f2  20838  coe1sfi  20842  coe1add  20893  coe1mul2lem1  20896  coe1mul2lem2  20897  coe1mul2  20898  ply1coe  20925  evls1rhmlem  20945  evl1sca  20958  evl1var  20960  pf1mpf  20976  pf1ind  20979  mat0dimscm  21074  mat0dimcrng  21075  mat0scmat  21143  mavmul0  21157  mavmul0g  21158  mvmumamul1  21159  mdet0pr  21197  mdet0f1o  21198  mdet0fv0  21199  mdetunilem9  21225  d0mat2pmat  21343  chpmat0d  21439  en1top  21589  en2top  21590  sn0topon  21603  indistopon  21606  indistps  21616  indistps2  21617  sn0cld  21695  indiscld  21696  neipeltop  21734  rest0  21774  restsn  21775  cmpfi  22013  refun0  22120  txindislem  22238  hmphindis  22402  xpstopnlem1  22414  xpstopnlem2  22416  ptcmpfi  22418  snfil  22469  fbasfip  22473  fgcl  22483  filconn  22488  fbasrn  22489  cfinfil  22498  csdfil  22499  supfil  22500  ufildr  22536  fin1aufil  22537  rnelfmlem  22557  fclsval  22613  tmdgsum  22700  tsmsfbas  22733  ust0  22825  ustn0  22826  0met  22973  xpsdsval  22988  minveclem3b  24032  tdeglem2  24662  deg1ldg  24693  deg1leb  24696  deg1val  24697  ulm0  24986  uhgr0  26866  upgr0eop  26907  upgr0eopALT  26909  usgr0  27033  usgr0eop  27036  lfuhgr1v0e  27044  griedg0prc  27054  0grsubgr  27068  cplgr0  27215  0grrusgr  27369  clwwlk0on0  27877  0ewlk  27899  0wlkon  27905  0trlon  27909  0pthon  27912  0pthonv  27914  0conngr  27977  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  wlkl0  28152  disjdifprg  30338  disjun0  30358  fpwrelmapffslem  30494  f1ocnt  30551  resvsca  30954  locfinref  31194  zarcmplem  31234  esumnul  31417  esumrnmpt2  31437  prsiga  31500  ldsysgenld  31529  ldgenpisyslem1  31532  oms0  31665  carsggect  31686  eulerpartgbij  31740  eulerpartlemmf  31743  repr0  31992  breprexp  32014  bnj941  32154  bnj97  32248  bnj149  32257  bnj150  32258  bnj944  32320  derang0  32529  indispconn  32594  goeleq12bg  32709  satf0  32732  satf0op  32737  fmla0  32742  fmla0xp  32743  fmlasuc0  32744  fmlafvel  32745  fmlasuc  32746  fmlaomn0  32750  fmla0disjsuc  32758  satfdmfmla  32760  satfv0fvfmla0  32773  sate0  32775  sate0fv0  32777  sategoelfvb  32779  ex-sategoelel  32781  prv0  32790  prv1n  32791  rdgprc  33152  dfrdg3  33154  trpredpred  33180  trpred0  33188  nosgnn0  33278  nodense  33309  nolt02o  33312  nulsslt  33375  nulssgt  33376  fullfunfnv  33520  fullfunfv  33521  rank0  33744  ssoninhaus  33909  onint1  33910  bj-0nel1  34389  bj-xpnzex  34395  bj-eltag  34413  bj-0eltag  34414  bj-tagss  34416  bj-pr1val  34440  bj-nuliota  34474  bj-nuliotaALT  34475  bj-rest10  34503  bj-rest10b  34504  bj-rest0  34508  rdgssun  34795  finxpreclem1  34806  finxpreclem2  34807  finxp0  34808  finxpreclem5  34812  poimirlem28  35085  heibor1lem  35247  heiborlem6  35254  reheibor  35277  n0elqs  35743  mzpcompact2lem  39692  wopprc  39971  pw2f1ocnv  39978  pwslnmlem0  40035  pwfi2f1o  40040  clsk1indlem0  40744  clsk1indlem4  40747  clsk1indlem1  40748  mnupwd  40975  mnuprdlem1  40980  mnuprdlem2  40981  mnuprdlem3  40982  mnurnd  40991  fnchoice  41658  eliuniincex  41745  limsup0  42336  0cnv  42384  liminf0  42435  0cnf  42519  dvnprodlem3  42590  qndenserrnbl  42937  prsal  42960  intsal  42970  sge00  43015  sge0sn  43018  nnfoctbdjlem  43094  isomenndlem  43169  hoiqssbl  43264  ovnsubadd2lem  43284  iota0def  43630  aiota0def  43651  afv0fv0  43705  0nelsetpreimafv  43907  lincval0  44824  lco0  44836  linds0  44874  0aryfvalel  45048  0aryfvalelfv  45049  1aryenef  45059  2aryenef  45070  bnd2d  45211