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

Theorem noel 3434
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 3273 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3274 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3431 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2322 . 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 2763    \ cdif 3124   (/)c0 3430
This theorem is referenced by:  n0i  3435  n0f  3438  rex0  3443  abvor0  3447  rab0  3450  un0  3454  in0  3455  0ss  3458  disj  3470  r19.2zb  3519  ral0  3533  int0  3850  iun0  3932  0iun  3933  ord0eln0  4418  nlim0  4422  nsuceq0  4444  xp0r  4756  dm0  4880  dm0rn0  4883  reldm0  4884  elimasni  5028  cnv0  5072  co02  5173  fv01  5493  mpt20  6133  tz7.44-2  6388  0we1  6473  omordi  6532  omeulem1  6548  nnmordi  6597  omabs  6613  omsmolem  6619  0er  6663  omxpenlem  6931  cantnfle  7340  en3lp  7386  r1sdom  7414  r1pwss  7424  alephordi  7669  axdc3lem2  8045  zorn2lem7  8097  brdom3  8121  canthwe  8241  nlt1pi  8498  xrinfm0  10622  elixx3g  10636  elfz2  10756  om2uzlti  10980  hashf1lem2  11360  sum0  12160  fsumsplit  12178  sumsplit  12197  fsum2dlem  12199  sadc0  12608  sadcp1  12609  saddisjlem  12618  smu01lem  12639  smu01  12640  smu02  12641  prmreclem5  12930  vdwap0  12986  ram0  13032  0catg  13552  oduclatb  14211  0g0  14349  cntzrcl  14766  gexdvds  14858  gsumzsplit  15169  dprdcntz2  15236  00lss  15662  mplcoe1  16172  mplcoe2  16174  mplrcl  16194  strov2rcl  16278  00ply1bas  16281  0ntop  16614  haust1  17043  hauspwdom  17190  kqcldsat  17387  tsmssplit  17797  0met  17893  itg11  19009  itg0  19097  bddmulibl  19156  fsumharmonic  20268  ppiublem2  20405  lgsdir2lem3  20527  helloworld  20799  eupath2lem1  23274  funpartfv  23859  elioo1t3  24870  0ded  25125  0catOLD  25126  pw2f1ocnv  26498  dsmmbas2  26571  dsmmfi  26572  pmtrfrn  26768  psgnunilem5  26785  stoweidlem34  27152  en3lpVD  27754
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-dif 3130  df-nul 3431
  Copyright terms: Public domain W3C validator