MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noel Unicode version

Theorem noel 3568
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
Assertion
Ref Expression
noel  |-  -.  A  e.  (/)

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3405 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3406 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3565 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2444 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 291 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1717   _Vcvv 2892    \ cdif 3253   (/)c0 3564
This theorem is referenced by:  n0i  3569  n0f  3572  rex0  3577  abvor0  3581  rab0  3584  un0  3588  in0  3589  0ss  3592  disj  3604  r19.2zb  3654  ral0  3668  int0  3999  iun0  4081  0iun  4082  ord0eln0  4569  nlim0  4573  nsuceq0  4595  xp0r  4889  dm0  5016  dm0rn0  5019  reldm0  5020  elimasni  5164  cnv0  5208  co02  5316  dffv3  5657  fv01  5695  bropopvvv  6358  mpt20  6359  tz7.44-2  6594  0we1  6679  omordi  6738  omeulem1  6754  nnmordi  6803  omabs  6819  omsmolem  6825  0er  6869  omxpenlem  7138  cantnfle  7552  en3lp  7598  r1sdom  7626  r1pwss  7636  alephordi  7881  axdc3lem2  8257  zorn2lem7  8308  brdom3  8332  canthwe  8452  nlt1pi  8709  xrinfm0  10840  elixx3g  10854  elfz2  10975  om2uzlti  11210  hashf1lem2  11625  sum0  12435  fsumsplit  12453  sumsplit  12472  fsum2dlem  12474  sadc0  12886  sadcp1  12887  saddisjlem  12896  smu01lem  12917  smu01  12918  smu02  12919  prmreclem5  13208  vdwap0  13264  ram0  13310  0catg  13832  oduclatb  14491  0g0  14629  cntzrcl  15046  gexdvds  15138  gsumzsplit  15449  dprdcntz2  15516  00lss  15938  mplcoe1  16448  mplcoe2  16450  mplrcl  16470  strov2rcl  16551  00ply1bas  16554  0ntop  16894  haust1  17331  hauspwdom  17478  kqcldsat  17679  tsmssplit  18095  ustn0  18164  0met  18297  itg11  19443  itg0  19531  bddmulibl  19590  fsumharmonic  20710  ppiublem2  20847  lgsdir2lem3  20969  nbgra0edg  21303  uvtx01vtx  21360  eupath2lem1  21540  helloworld  21600  measvuni  24355  prod0  25041  pw2f1ocnv  26792  dsmmbas2  26865  dsmmfi  26866  pmtrfrn  27062  psgnunilem5  27079  stoweidlem34  27444  en3lpVD  28291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259  df-nul 3565
  Copyright terms: Public domain W3C validator