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

Theorem noel 3459
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 3298 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3299 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 165 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3456 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2347 . 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 1684   _Vcvv 2788    \ cdif 3149   (/)c0 3455
This theorem is referenced by:  n0i  3460  n0f  3463  rex0  3468  abvor0  3472  rab0  3475  un0  3479  in0  3480  0ss  3483  disj  3495  r19.2zb  3544  ral0  3558  int0  3876  iun0  3958  0iun  3959  ord0eln0  4446  nlim0  4450  nsuceq0  4472  xp0r  4768  dm0  4892  dm0rn0  4895  reldm0  4896  elimasni  5040  cnv0  5084  co02  5186  dffv3  5521  fv01  5559  mpt20  6199  tz7.44-2  6420  0we1  6505  omordi  6564  omeulem1  6580  nnmordi  6629  omabs  6645  omsmolem  6651  0er  6695  omxpenlem  6963  cantnfle  7372  en3lp  7418  r1sdom  7446  r1pwss  7456  alephordi  7701  axdc3lem2  8077  zorn2lem7  8129  brdom3  8153  canthwe  8273  nlt1pi  8530  xrinfm0  10655  elixx3g  10669  elfz2  10789  om2uzlti  11013  hashf1lem2  11394  sum0  12194  fsumsplit  12212  sumsplit  12231  fsum2dlem  12233  sadc0  12645  sadcp1  12646  saddisjlem  12655  smu01lem  12676  smu01  12677  smu02  12678  prmreclem5  12967  vdwap0  13023  ram0  13069  0catg  13589  oduclatb  14248  0g0  14386  cntzrcl  14803  gexdvds  14895  gsumzsplit  15206  dprdcntz2  15273  00lss  15699  mplcoe1  16209  mplcoe2  16211  mplrcl  16231  strov2rcl  16315  00ply1bas  16318  0ntop  16651  haust1  17080  hauspwdom  17227  kqcldsat  17424  tsmssplit  17834  0met  17930  itg11  19046  itg0  19134  bddmulibl  19193  fsumharmonic  20305  ppiublem2  20442  lgsdir2lem3  20564  helloworld  20838  measvuni  23542  eupath2lem1  23901  funpartfv  24483  elioo1t3  25502  0ded  25757  0catOLD  25758  pw2f1ocnv  27130  dsmmbas2  27203  dsmmfi  27204  pmtrfrn  27400  psgnunilem5  27417  stoweidlem34  27783  nbgra0edg  28147  uvtx01vtx  28164  en3lpVD  28621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator