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

Theorem 0ex 4760
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 4759. (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 4759 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 3911 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1771 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 221 . 2 𝑥 𝑥 = ∅
54issetri 3200 1 ∅ ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1478   = wceq 1480  wex 1701  wcel 1987  Vcvv 3190  c0 3897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-nul 3898
This theorem is referenced by:  sseliALT  4761  csbexg  4762  unisn2  4764  class2set  4802  0elpw  4804  0nep0  4806  unidif0  4808  iin0  4809  notzfaus  4810  intv  4811  snexALT  4822  p0ex  4823  dtruALT  4870  zfpair  4875  snex  4879  dtruALT2  4882  opex  4903  opthwiener  4946  opthprc  5137  dmsnsnsn  5582  0elon  5747  nsuceq0  5774  snsn0non  5815  iotaex  5837  nfunv  5889  fun0  5922  fvrn0  6183  fvssunirn  6184  fprg  6387  ovima0  6778  onint0  6958  tfinds2  7025  finds  7054  finds2  7056  xpexr  7068  soex  7071  supp0  7260  fvn0elsupp  7271  fvn0elsuppb  7272  brtpos0  7319  reldmtpos  7320  tfrlem16  7449  tz7.44-1  7462  seqomlem1  7505  1n0  7535  el1o  7539  om0  7557  mapdm0  7832  map0e  7855  ixpexg  7892  0elixp  7899  en0  7979  ensn1  7980  en1  7983  2dom  7989  map1  7996  xp1en  8006  endisj  8007  pw2eng  8026  map2xp  8090  limensuci  8096  1sdom  8123  unxpdom2  8128  sucxpdom  8129  isinf  8133  ac6sfi  8164  fodomfi  8199  0fsupp  8257  fi0  8286  oiexg  8400  brwdom  8432  brwdom2  8438  inf3lemb  8482  infeq5i  8493  dfom3  8504  cantnfvalf  8522  cantnfval2  8526  cantnfle  8528  cantnflt  8529  cantnff  8531  cantnf0  8532  cantnfp1lem1  8535  cantnfp1lem2  8536  cantnfp1lem3  8537  cantnfp1  8538  cantnflem1a  8542  cantnflem1d  8545  cantnflem1  8546  cantnflem3  8548  cantnf  8550  cnfcomlem  8556  cnfcom  8557  cnfcom2lem  8558  cnfcom3  8561  tc0  8583  r10  8591  scottex  8708  infxpenlem  8796  fseqenlem1  8807  uncdadom  8953  cdaun  8954  cdaen  8955  cda1dif  8958  pm110.643  8959  cda0en  8961  cdacomen  8963  cdaassen  8964  xpcdaen  8965  mapcdaen  8966  cdaxpdom  8971  cdainf  8974  infcda1  8975  pwsdompw  8986  pwcdadom  8998  ackbij1lem14  9015  ackbij2lem2  9022  ackbij2lem3  9023  cf0  9033  cfeq0  9038  cfsuc  9039  cflim2  9045  isfin5  9081  isfin4-3  9097  fin1a2lem11  9192  fin1a2lem12  9193  fin1a2lem13  9194  axcc2lem  9218  ac6num  9261  zornn0g  9287  ttukeylem3  9293  brdom3  9310  iundom2g  9322  cardeq0  9334  alephadd  9359  pwcfsdom  9365  axpowndlem3  9381  canthwe  9433  canthp1lem1  9434  pwxpndom2  9447  pwcdandom  9449  gchxpidm  9451  intwun  9517  0tsk  9537  grothomex  9611  indpi  9689  fzennn  12723  hash0  13114  hashen1  13116  hashmap  13178  hashbc  13191  hashf1  13195  hashge3el3dif  13222  swrdval  13371  swrd00  13372  swrd0  13388  cshfn  13489  cshnz  13491  0csh0  13492  incexclem  14512  incexc  14513  rexpen  14901  sadcf  15118  sadc0  15119  sadcp1  15120  smupf  15143  smup0  15144  smupp1  15145  0ram  15667  ram0  15669  cshws0  15751  str0  15851  ressbas  15870  ress0  15874  0rest  16030  xpscg  16158  xpscfn  16159  xpsc0  16160  xpsc1  16161  xpsfrnel  16163  xpsfrnel2  16165  xpsle  16181  ismred2  16203  acsfn  16260  0cat  16289  ciclcl  16402  cicrcl  16403  cicer  16406  setcepi  16678  0pos  16894  meet0  17077  join0  17078  mgm0b  17196  gsum0  17218  sgrp0b  17232  ga0  17671  psgn0fv0  17871  pmtrsn  17879  oppglsm  17997  efgi0  18073  vrgpf  18121  vrgpinv  18122  frgpuptinv  18124  frgpup2  18129  0frgp  18132  frgpnabllem1  18216  frgpnabllem2  18217  dprd0  18370  dmdprdpr  18388  dprdpr  18389  00lsp  18921  fvcoe1  19517  coe1f2  19519  coe1sfi  19523  coe1add  19574  coe1mul2lem1  19577  coe1mul2lem2  19578  coe1mul2  19579  ply1coe  19606  evls1rhmlem  19626  evl1sca  19638  evl1var  19640  pf1mpf  19656  pf1ind  19659  cnfldfunALT  19699  frgpcyg  19862  frlmiscvec  20128  mat0dimscm  20215  mat0dimcrng  20216  mat0scmat  20284  mavmul0  20298  mavmul0g  20299  mvmumamul1  20300  mdet0pr  20338  mdet0f1o  20339  mdet0fv0  20340  mdetunilem9  20366  d0mat2pmat  20483  chpmat0d  20579  topgele  20674  en1top  20728  en2top  20729  sn0topon  20742  indistopon  20745  indistps  20755  indistps2  20756  sn0cld  20834  indiscld  20835  neipeltop  20873  rest0  20913  restsn  20914  cmpfi  21151  refun0  21258  txindislem  21376  hmphindis  21540  xpstopnlem1  21552  xpstopnlem2  21554  ptcmpfi  21556  snfil  21608  fbasfip  21612  fgcl  21622  filconn  21627  fbasrn  21628  cfinfil  21637  csdfil  21638  supfil  21639  ufildr  21675  fin1aufil  21676  rnelfmlem  21696  fclsval  21752  tmdgsum  21839  tsmsfbas  21871  ust0  21963  ustn0  21964  0met  22111  xpsdsval  22126  minveclem3b  23139  tdeglem2  23759  deg1ldg  23790  deg1leb  23793  deg1val  23794  ulm0  24083  uhgr0  25898  upgr0eop  25938  upgr0eopALT  25940  usgr0  26062  usgr0eop  26065  lfuhgr1v0e  26073  griedg0prc  26083  0grsubgr  26097  cplgr0  26242  0grrusgr  26379  0ewlk  26875  0wlkon  26881  0trlon  26885  0pthon  26888  0pthonv  26890  0conngr  26952  konigsberglem1  27014  konigsberglem2  27015  konigsberglem3  27016  disjdifprg  29274  disjun0  29294  fpwrelmapffslem  29391  f1ocnt  29442  resvsca  29657  locfinref  29732  esumnul  29933  esumrnmpt2  29953  prsiga  30017  ldsysgenld  30046  ldgenpisyslem1  30049  oms0  30182  carsggect  30203  eulerpartgbij  30257  eulerpartlemmf  30260  brepr0  30500  bnj941  30604  bnj97  30697  bnj149  30706  bnj150  30707  bnj944  30769  derang0  30912  indispconn  30977  rdgprc  31454  dfrdg3  31456  trpredpred  31482  trpred0  31490  nosgnn0  31565  nodense  31605  fullfunfnv  31748  fullfunfv  31749  rank0  31972  ssoninhaus  32142  onint1  32143  bj-1ex  32638  bj-0nel1  32640  bj-xpnzex  32646  bj-eltag  32665  bj-0eltag  32666  bj-tagss  32668  bj-pr1val  32692  bj-nuliota  32719  bj-nuliotaALT  32720  bj-rest10  32731  bj-rest10b  32732  bj-rest0  32736  finxpreclem1  32897  finxpreclem2  32898  finxp0  32899  finxpreclem5  32903  poimirlem28  33108  heibor1lem  33279  heiborlem6  33286  reheibor  33309  mzpcompact2lem  36833  wopprc  37116  pw2f1ocnv  37123  pwslnmlem0  37180  pwfi2f1o  37185  relintabex  37407  clsk1indlem0  37860  clsk1indlem4  37863  clsk1indlem1  37864  fnchoice  38710  eliuniincex  38816  mapdm0OLD  38892  limsup0  39362  0cnf  39425  dvnprodlem3  39500  qndenserrnbl  39852  prsal  39875  intsal  39885  sge00  39930  sge0sn  39933  nnfoctbdjlem  40009  isomenndlem  40081  hoiqssbl  40176  ovnsubadd2lem  40196  afv0fv0  40563  lincval0  41522  lco0  41534  linds0  41572  bnd2d  41750
  Copyright terms: Public domain W3C validator