MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ex Structured version   Visualization version   GIF version

Theorem 0ex 4823
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 4822. (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.
StepHypRef Expression
1 ax-nul 4822 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 3962 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1814 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 221 . 2 𝑥 𝑥 = ∅
54issetri 3241 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1521   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  sseliALT  4824  csbexg  4825  unisn2  4827  class2set  4862  0elpw  4864  0nep0  4866  unidif0  4868  iin0  4869  notzfaus  4870  intv  4871  snexALT  4882  p0ex  4883  dtruALT  4929  zfpair  4934  snex  4938  dtruALT2  4941  opex  4962  opthwiener  5005  opthprc  5201  nrelv  5277  dmsnsnsn  5649  0elon  5816  nsuceq0  5843  snsn0non  5884  iotaex  5906  nfunv  5959  fun0  5992  fvrn0  6254  fvssunirn  6255  fprg  6462  ovima0  6855  onint0  7038  tfinds2  7105  finds  7134  finds2  7136  xpexr  7148  soex  7151  supp0  7345  fvn0elsupp  7356  fvn0elsuppb  7357  brtpos0  7404  reldmtpos  7405  tfrlem16  7534  tz7.44-1  7547  seqomlem1  7590  1n0  7620  el1o  7624  om0  7642  mapdm0  7914  map0e  7937  ixpexg  7974  0elixp  7981  en0  8060  ensn1  8061  en1  8064  2dom  8070  map1  8077  xp1en  8087  endisj  8088  pw2eng  8107  map2xp  8171  limensuci  8177  1sdom  8204  unxpdom2  8209  sucxpdom  8210  isinf  8214  ac6sfi  8245  fodomfi  8280  0fsupp  8338  fi0  8367  oiexg  8481  brwdom  8513  brwdom2  8519  inf3lemb  8560  infeq5i  8571  dfom3  8582  cantnfvalf  8600  cantnfval2  8604  cantnfle  8606  cantnflt  8607  cantnff  8609  cantnf0  8610  cantnfp1lem1  8613  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnfp1  8616  cantnflem1a  8620  cantnflem1d  8623  cantnflem1  8624  cantnflem3  8626  cantnf  8628  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom3  8639  tc0  8661  r10  8669  scottex  8786  infxpenlem  8874  fseqenlem1  8885  uncdadom  9031  cdaun  9032  cdaen  9033  cda1dif  9036  pm110.643  9037  cda0en  9039  cdacomen  9041  cdaassen  9042  xpcdaen  9043  mapcdaen  9044  cdaxpdom  9049  cdainf  9052  infcda1  9053  pwsdompw  9064  pwcdadom  9076  ackbij1lem14  9093  ackbij2lem2  9100  ackbij2lem3  9101  cf0  9111  cfeq0  9116  cfsuc  9117  cflim2  9123  isfin5  9159  isfin4-3  9175  fin1a2lem11  9270  fin1a2lem12  9271  fin1a2lem13  9272  axcc2lem  9296  ac6num  9339  zornn0g  9365  ttukeylem3  9371  brdom3  9388  iundom2g  9400  cardeq0  9412  alephadd  9437  pwcfsdom  9443  axpowndlem3  9459  canthwe  9511  canthp1lem1  9512  pwxpndom2  9525  pwcdandom  9527  gchxpidm  9529  intwun  9595  0tsk  9615  grothomex  9689  indpi  9767  fzennn  12807  hash0  13196  hashen1  13198  hashmap  13260  hashbc  13275  hashf1  13279  hashge3el3dif  13306  ccat1st1st  13448  swrdval  13462  swrd00  13463  swrd0  13480  cshfn  13582  cshnz  13584  0csh0  13585  incexclem  14612  incexc  14613  rexpen  15001  sadcf  15222  sadc0  15223  sadcp1  15224  smupf  15247  smup0  15248  smupp1  15249  0ram  15771  ram0  15773  cshws0  15855  str0  15958  ressbas  15977  ress0  15981  0rest  16137  xpscg  16265  xpscfn  16266  xpsc0  16267  xpsc1  16268  xpsfrnel  16270  xpsfrnel2  16272  xpsle  16288  ismred2  16310  acsfn  16367  0cat  16396  ciclcl  16509  cicrcl  16510  cicer  16513  setcepi  16785  0pos  17001  meet0  17184  join0  17185  mgm0b  17303  gsum0  17325  sgrp0b  17339  ga0  17777  psgn0fv0  17977  pmtrsn  17985  oppglsm  18103  efgi0  18179  vrgpf  18227  vrgpinv  18228  frgpuptinv  18230  frgpup2  18235  0frgp  18238  frgpnabllem1  18322  frgpnabllem2  18323  dprd0  18476  dmdprdpr  18494  dprdpr  18495  00lsp  19029  fvcoe1  19625  coe1f2  19627  coe1sfi  19631  coe1add  19682  coe1mul2lem1  19685  coe1mul2lem2  19686  coe1mul2  19687  ply1coe  19714  evls1rhmlem  19734  evl1sca  19746  evl1var  19748  pf1mpf  19764  pf1ind  19767  cnfldfunALT  19807  frgpcyg  19970  frlmiscvec  20236  mat0dimscm  20323  mat0dimcrng  20324  mat0scmat  20392  mavmul0  20406  mavmul0g  20407  mvmumamul1  20408  mdet0pr  20446  mdet0f1o  20447  mdet0fv0  20448  mdetunilem9  20474  d0mat2pmat  20591  chpmat0d  20687  topgele  20782  en1top  20836  en2top  20837  sn0topon  20850  indistopon  20853  indistps  20863  indistps2  20864  sn0cld  20942  indiscld  20943  neipeltop  20981  rest0  21021  restsn  21022  cmpfi  21259  refun0  21366  txindislem  21484  hmphindis  21648  xpstopnlem1  21660  xpstopnlem2  21662  ptcmpfi  21664  snfil  21715  fbasfip  21719  fgcl  21729  filconn  21734  fbasrn  21735  cfinfil  21744  csdfil  21745  supfil  21746  ufildr  21782  fin1aufil  21783  rnelfmlem  21803  fclsval  21859  tmdgsum  21946  tsmsfbas  21978  ust0  22070  ustn0  22071  0met  22218  xpsdsval  22233  minveclem3b  23245  tdeglem2  23866  deg1ldg  23897  deg1leb  23900  deg1val  23901  ulm0  24190  uhgr0  26013  upgr0eop  26054  upgr0eopALT  26056  usgr0  26180  usgr0eop  26183  lfuhgr1v0e  26191  griedg0prc  26201  0grsubgr  26215  cplgr0  26377  0grrusgr  26531  clwwlk0on0  27067  0ewlk  27092  0wlkon  27098  0trlon  27102  0pthon  27105  0pthonv  27107  0conngr  27170  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  disjdifprg  29514  disjun0  29534  fpwrelmapffslem  29635  f1ocnt  29687  resvsca  29958  locfinref  30036  esumnul  30238  esumrnmpt2  30258  prsiga  30322  ldsysgenld  30351  ldgenpisyslem1  30354  oms0  30487  carsggect  30508  eulerpartgbij  30562  eulerpartlemmf  30565  repr0  30817  breprexp  30839  bnj941  30969  bnj97  31062  bnj149  31071  bnj150  31072  bnj944  31134  derang0  31277  indispconn  31342  rdgprc  31824  dfrdg3  31826  trpredpred  31852  trpred0  31860  nosgnn0  31936  nodense  31967  nolt02o  31970  nulsslt  32033  nulssgt  32034  fullfunfnv  32178  fullfunfv  32179  rank0  32402  ssoninhaus  32572  onint1  32573  bj-1ex  33063  bj-0nel1  33065  bj-xpnzex  33071  bj-eltag  33090  bj-0eltag  33091  bj-tagss  33093  bj-pr1val  33117  bj-nuliota  33144  bj-nuliotaALT  33145  bj-rest10  33166  bj-rest10b  33167  bj-rest0  33171  finxpreclem1  33356  finxpreclem2  33357  finxp0  33358  finxpreclem5  33362  poimirlem28  33567  heibor1lem  33738  heiborlem6  33745  reheibor  33768  n0elqs  34239  mzpcompact2lem  37631  wopprc  37914  pw2f1ocnv  37921  pwslnmlem0  37978  pwfi2f1o  37983  relintabex  38204  clsk1indlem0  38656  clsk1indlem4  38659  clsk1indlem1  38660  fnchoice  39502  eliuniincex  39606  mapdm0OLD  39697  limsup0  40244  0cnv  40292  liminf0  40343  0cnf  40408  dvnprodlem3  40481  qndenserrnbl  40833  prsal  40856  intsal  40866  sge00  40911  sge0sn  40914  nnfoctbdjlem  40990  isomenndlem  41065  hoiqssbl  41160  ovnsubadd2lem  41180  afv0fv0  41550  lincval0  42529  lco0  42541  linds0  42579  bnd2d  42753
  Copyright terms: Public domain W3C validator