Theorem 0ex 5211

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 5210. (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 5210	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4308	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 233	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3510	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3494  ∅c0 4291

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-nul 4292

This theorem is referenced by:  al0ssb  5212  sseliALT  5213  csbexg  5214  unisn2  5216  class2set  5254  0elpw  5256  0nep0  5258  unidif0  5260  iin0  5261  notzfaus  5262  notzfausOLD  5263  intv  5264  snexALT  5284  p0ex  5285  dtruALT  5289  zfpair  5322  snex  5332  dtruALT2  5336  opex  5356  opthwiener  5404  0sn0ep  5470  opthprc  5616  nrelv  5673  dmsnsnsn  6077  0elon  6244  nsuceq0  6271  snsn0non  6309  iotaex  6335  fun0  6419  fvrn0  6698  fvssunirn  6699  fprg  6917  ovima0  7327  onint0  7511  tfinds2  7578  finds  7608  finds2  7610  xpexr  7623  soex  7626  supp0  7835  fvn0elsupp  7846  fvn0elsuppb  7847  brtpos0  7899  reldmtpos  7900  tfrlem16  8029  tz7.44-1  8042  seqomlem1  8086  1n0  8119  el1o  8124  om0  8142  mapdm0  8421  0map0sn0  8449  ixpexg  8486  0elixp  8493  en0  8572  ensn1  8573  en1  8576  2dom  8582  map1  8592  xp1en  8603  endisj  8604  pw2eng  8623  map2xp  8687  limensuci  8693  1sdom  8721  unxpdom2  8726  sucxpdom  8727  isinf  8731  ac6sfi  8762  fodomfi  8797  0fsupp  8855  fi0  8884  oiexg  8999  brwdom  9031  brwdom2  9037  inf3lemb  9088  infeq5i  9099  dfom3  9110  cantnfvalf  9128  cantnfval2  9132  cantnfle  9134  cantnflt  9135  cantnff  9137  cantnf0  9138  cantnfp1lem1  9141  cantnfp1lem3  9143  cantnfp1  9144  cantnflem1a  9148  cantnflem1d  9151  cantnflem1  9152  cantnf  9156  cnfcomlem  9162  cnfcom  9163  cnfcom2lem  9164  cnfcom3  9167  tc0  9189  r10  9197  scottex  9314  djulcl  9339  djulf1o  9341  djuss  9349  djuun  9355  1stinl  9356  2ndinl  9357  infxpenlem  9439  fseqenlem1  9450  undjudom  9593  endjudisj  9594  djuen  9595  dju1dif  9598  dju1p1e2  9599  dju0en  9601  djucomen  9603  djuassen  9604  xpdjuen  9605  mapdjuen  9606  djuxpdom  9611  djuinf  9614  infdju1  9615  djulepw  9618  pwsdompw  9626  pwdjudom  9638  ackbij1lem14  9655  ackbij2lem2  9662  ackbij2lem3  9663  cf0  9673  cfeq0  9678  cfsuc  9679  cflim2  9685  isfin5  9721  isfin4p1  9737  fin1a2lem11  9832  fin1a2lem12  9833  fin1a2lem13  9834  axcc2lem  9858  ac6num  9901  zornn0g  9927  ttukeylem3  9933  brdom3  9950  iundom2g  9962  cardeq0  9974  pwcfsdom  10005  axpowndlem3  10021  canthwe  10073  canthp1lem1  10074  pwxpndom2  10087  pwdjundom  10089  gchxpidm  10091  intwun  10157  0tsk  10177  grothomex  10251  indpi  10329  fzennn  13337  hash0  13729  hashen1  13732  hashmap  13797  hashbc  13812  hashf1  13816  hashge3el3dif  13845  ccat1st1st  13984  swrdval  14005  swrd00  14006  swrd0  14020  cshfn  14152  cshnz  14154  0csh0  14155  incexclem  15191  incexc  15192  rexpen  15581  sadcf  15802  sadc0  15803  sadcp1  15804  smupf  15827  smup0  15828  smupp1  15829  0ram  16356  ram0  16358  cshws0  16435  str0  16535  ressbas  16554  ress0  16558  0rest  16703  fnpr2ob  16831  xpsfrnel  16835  xpsle  16852  ismred2  16874  acsfn  16930  0cat  16959  ciclcl  17072  cicrcl  17073  cicer  17076  setcepi  17348  0pos  17564  meet0  17747  join0  17748  mgm0b  17867  gsum0  17894  sgrp0b  17909  efmnd0nmnd  18055  pwmnd  18102  mulgfval  18226  ga0  18428  psgn0fv0  18639  pmtrsn  18647  oppglsm  18767  efgi0  18846  vrgpf  18894  vrgpinv  18895  frgpuptinv  18897  frgpup2  18902  0frgp  18905  frgpnabllem1  18993  frgpnabllem2  18994  dprd0  19153  dmdprdpr  19171  dprdpr  19172  00lsp  19753  fvcoe1  20375  coe1f2  20377  coe1sfi  20381  coe1add  20432  coe1mul2lem1  20435  coe1mul2lem2  20436  coe1mul2  20437  ply1coe  20464  evls1rhmlem  20484  evl1sca  20497  evl1var  20499  pf1mpf  20515  pf1ind  20518  cnfldfunALT  20558  frgpcyg  20720  frlmiscvec  20993  mat0dimscm  21078  mat0dimcrng  21079  mat0scmat  21147  mavmul0  21161  mavmul0g  21162  mvmumamul1  21163  mdet0pr  21201  mdet0f1o  21202  mdet0fv0  21203  mdetunilem9  21229  d0mat2pmat  21346  chpmat0d  21442  en1top  21592  en2top  21593  sn0topon  21606  indistopon  21609  indistps  21619  indistps2  21620  sn0cld  21698  indiscld  21699  neipeltop  21737  rest0  21777  restsn  21778  cmpfi  22016  refun0  22123  txindislem  22241  hmphindis  22405  xpstopnlem1  22417  xpstopnlem2  22419  ptcmpfi  22421  snfil  22472  fbasfip  22476  fgcl  22486  filconn  22491  fbasrn  22492  cfinfil  22501  csdfil  22502  supfil  22503  ufildr  22539  fin1aufil  22540  rnelfmlem  22560  fclsval  22616  tmdgsum  22703  tsmsfbas  22736  ust0  22828  ustn0  22829  0met  22976  xpsdsval  22991  minveclem3b  24031  tdeglem2  24655  deg1ldg  24686  deg1leb  24689  deg1val  24690  ulm0  24979  uhgr0  26858  upgr0eop  26899  upgr0eopALT  26901  usgr0  27025  usgr0eop  27028  lfuhgr1v0e  27036  griedg0prc  27046  0grsubgr  27060  cplgr0  27207  0grrusgr  27361  clwwlk0on0  27871  0ewlk  27893  0wlkon  27899  0trlon  27903  0pthon  27906  0pthonv  27908  0conngr  27971  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  wlkl0  28146  disjdifprg  30325  disjun0  30345  fpwrelmapffslem  30468  f1ocnt  30525  resvsca  30903  locfinref  31105  esumnul  31307  esumrnmpt2  31327  prsiga  31390  ldsysgenld  31419  ldgenpisyslem1  31422  oms0  31555  carsggect  31576  eulerpartgbij  31630  eulerpartlemmf  31633  repr0  31882  breprexp  31904  bnj941  32044  bnj97  32138  bnj149  32147  bnj150  32148  bnj944  32210  derang0  32416  indispconn  32481  goeleq12bg  32596  satf0  32619  satf0op  32624  fmla0  32629  fmla0xp  32630  fmlasuc0  32631  fmlafvel  32632  fmlasuc  32633  fmlaomn0  32637  fmla0disjsuc  32645  satfdmfmla  32647  satfv0fvfmla0  32660  sate0  32662  sate0fv0  32664  sategoelfvb  32666  ex-sategoelel  32668  prv0  32677  prv1n  32678  rdgprc  33039  dfrdg3  33041  trpredpred  33067  trpred0  33075  nosgnn0  33165  nodense  33196  nolt02o  33199  nulsslt  33262  nulssgt  33263  fullfunfnv  33407  fullfunfv  33408  rank0  33631  ssoninhaus  33796  onint1  33797  bj-0nel1  34268  bj-xpnzex  34274  bj-eltag  34292  bj-0eltag  34293  bj-tagss  34295  bj-pr1val  34319  bj-nuliota  34353  bj-nuliotaALT  34354  bj-rest10  34382  bj-rest10b  34383  bj-rest0  34387  rdgssun  34662  finxpreclem1  34673  finxpreclem2  34674  finxp0  34675  finxpreclem5  34679  poimirlem28  34935  heibor1lem  35102  heiborlem6  35109  reheibor  35132  n0elqs  35598  mzpcompact2lem  39397  wopprc  39676  pw2f1ocnv  39683  pwslnmlem0  39740  pwfi2f1o  39745  clsk1indlem0  40440  clsk1indlem4  40443  clsk1indlem1  40444  mnupwd  40652  mnuprdlem1  40657  mnuprdlem2  40658  mnuprdlem3  40659  mnurnd  40668  fnchoice  41335  eliuniincex  41424  limsup0  42024  0cnv  42072  liminf0  42123  0cnf  42209  dvnprodlem3  42282  qndenserrnbl  42629  prsal  42652  intsal  42662  sge00  42707  sge0sn  42710  nnfoctbdjlem  42786  isomenndlem  42861  hoiqssbl  42956  ovnsubadd2lem  42976  iota0def  43322  aiota0def  43343  afv0fv0  43397  0nelsetpreimafv  43599  lincval0  44519  lco0  44531  linds0  44569  bnd2d  44833