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

Theorem noel 3366
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 3215 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3216 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3363 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2317 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 292 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 5    e. wcel 1621   _Vcvv 2727    \ cdif 3075   (/)c0 3362
This theorem is referenced by:  n0i  3367  n0f  3370  rex0  3375  abvor0  3379  rab0  3382  un0  3386  in0  3387  0ss  3390  disj  3402  r19.2zb  3450  ral0  3464  int0  3774  iun0  3856  0iun  3857  ord0eln0  4339  nlim0  4343  nsuceq0  4365  xp0r  4675  dm0  4799  dm0rn0  4802  reldm0  4803  elimasni  4947  cnv0  4991  co02  5092  fv01  5411  mpt20  6051  tz7.44-2  6306  0we1  6391  omordi  6450  omeulem1  6466  nnmordi  6515  omabs  6531  omsmolem  6537  0er  6581  omxpenlem  6848  cantnfle  7256  en3lp  7302  r1sdom  7330  r1pwss  7340  alephordi  7585  axdc3lem2  7961  zorn2lem7  8013  brdom3  8037  canthwe  8153  nlt1pi  8410  xrinfm0  10533  elixx3g  10547  elfz2  10667  om2uzlti  10891  hashf1lem2  11271  sum0  12071  fsumsplit  12089  sumsplit  12108  fsum2dlem  12110  sadc0  12519  sadcp1  12520  saddisjlem  12529  smu01lem  12550  smu01  12551  smu02  12552  prmreclem5  12841  vdwap0  12897  ram0  12943  0catg  13433  oduclatb  14092  0g0  14221  cntzrcl  14638  gexdvds  14730  gsumzsplit  15041  dprdcntz2  15108  00lss  15534  mplcoe1  16041  mplcoe2  16043  mplrcl  16063  strov2rcl  16147  00ply1bas  16150  0ntop  16483  haust1  16912  hauspwdom  17059  kqcldsat  17256  tsmssplit  17666  0met  17762  itg11  18878  itg0  18966  bddmulibl  19025  fsumharmonic  20137  ppiublem2  20274  lgsdir2lem3  20396  helloworld  20668  eupath2lem1  23072  funpartfv  23657  elioo1t3  24668  0ded  24923  0catOLD  24924  pw2f1ocnv  26296  dsmmbas2  26369  dsmmfi  26370  pmtrfrn  26566  psgnunilem5  26583  en3lpVD  27311
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-nul 3363
  Copyright terms: Public domain W3C validator