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

Theorem noel 3547
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 3385 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3386 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 165 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3544 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2430 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 290 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1715   _Vcvv 2873    \ cdif 3235   (/)c0 3543
This theorem is referenced by:  n0i  3548  n0f  3551  rex0  3556  abvor0  3560  rab0  3563  un0  3567  in0  3568  0ss  3571  disj  3583  r19.2zb  3633  ral0  3647  int0  3978  iun0  4060  0iun  4061  ord0eln0  4549  nlim0  4553  nsuceq0  4575  xp0r  4871  dm0  4995  dm0rn0  4998  reldm0  4999  elimasni  5143  cnv0  5187  co02  5289  dffv3  5628  fv01  5666  bropopvvv  6326  mpt20  6327  tz7.44-2  6562  0we1  6647  omordi  6706  omeulem1  6722  nnmordi  6771  omabs  6787  omsmolem  6793  0er  6837  omxpenlem  7106  cantnfle  7519  en3lp  7565  r1sdom  7593  r1pwss  7603  alephordi  7848  axdc3lem2  8224  zorn2lem7  8276  brdom3  8300  canthwe  8420  nlt1pi  8677  xrinfm0  10808  elixx3g  10822  elfz2  10942  om2uzlti  11177  hashf1lem2  11592  sum0  12402  fsumsplit  12420  sumsplit  12439  fsum2dlem  12441  sadc0  12853  sadcp1  12854  saddisjlem  12863  smu01lem  12884  smu01  12885  smu02  12886  prmreclem5  13175  vdwap0  13231  ram0  13277  0catg  13799  oduclatb  14458  0g0  14596  cntzrcl  15013  gexdvds  15105  gsumzsplit  15416  dprdcntz2  15483  00lss  15909  mplcoe1  16419  mplcoe2  16421  mplrcl  16441  strov2rcl  16525  00ply1bas  16528  0ntop  16868  haust1  17297  hauspwdom  17444  kqcldsat  17641  tsmssplit  18047  0met  18143  itg11  19261  itg0  19349  bddmulibl  19408  fsumharmonic  20528  ppiublem2  20665  lgsdir2lem3  20787  helloworld  21149  ustn0  23723  measvuni  24031  eupath2lem1  24488  prod0  24753  pw2f1ocnv  26636  dsmmbas2  26709  dsmmfi  26710  pmtrfrn  26906  psgnunilem5  26923  stoweidlem34  27289  nbgra0edg  27600  uvtx01vtx  27657  en3lpVD  28385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-dif 3241  df-nul 3544
  Copyright terms: Public domain W3C validator