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

Theorem noel 3460
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 3299 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3300 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 165 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3457 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2348 . 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 1685   _Vcvv 2789    \ cdif 3150   (/)c0 3456
This theorem is referenced by:  n0i  3461  n0f  3464  rex0  3469  abvor0  3473  rab0  3476  un0  3480  in0  3481  0ss  3484  disj  3496  r19.2zb  3545  ral0  3559  int0  3877  iun0  3959  0iun  3960  ord0eln0  4445  nlim0  4449  nsuceq0  4471  xp0r  4767  dm0  4891  dm0rn0  4894  reldm0  4895  elimasni  5039  cnv0  5083  co02  5184  fv01  5521  mpt20  6161  tz7.44-2  6416  0we1  6501  omordi  6560  omeulem1  6576  nnmordi  6625  omabs  6641  omsmolem  6647  0er  6691  omxpenlem  6959  cantnfle  7368  en3lp  7414  r1sdom  7442  r1pwss  7452  alephordi  7697  axdc3lem2  8073  zorn2lem7  8125  brdom3  8149  canthwe  8269  nlt1pi  8526  xrinfm0  10651  elixx3g  10665  elfz2  10785  om2uzlti  11009  hashf1lem2  11390  sum0  12190  fsumsplit  12208  sumsplit  12227  fsum2dlem  12229  sadc0  12641  sadcp1  12642  saddisjlem  12651  smu01lem  12672  smu01  12673  smu02  12674  prmreclem5  12963  vdwap0  13019  ram0  13065  0catg  13585  oduclatb  14244  0g0  14382  cntzrcl  14799  gexdvds  14891  gsumzsplit  15202  dprdcntz2  15269  00lss  15695  mplcoe1  16205  mplcoe2  16207  mplrcl  16227  strov2rcl  16311  00ply1bas  16314  0ntop  16647  haust1  17076  hauspwdom  17223  kqcldsat  17420  tsmssplit  17830  0met  17926  itg11  19042  itg0  19130  bddmulibl  19189  fsumharmonic  20301  ppiublem2  20438  lgsdir2lem3  20560  helloworld  20832  eupath2lem1  23308  funpartfv  23893  elioo1t3  24913  0ded  25168  0catOLD  25169  pw2f1ocnv  26541  dsmmbas2  26614  dsmmfi  26615  pmtrfrn  26811  psgnunilem5  26828  stoweidlem34  27194  en3lpVD  27901
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator