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

Theorem noel 3596
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 3433 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3434 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3593 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2472 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 291 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1721   _Vcvv 2920    \ cdif 3281   (/)c0 3592
This theorem is referenced by:  n0i  3597  n0f  3600  rex0  3605  abvor0  3609  rab0  3612  un0  3616  in0  3617  0ss  3620  disj  3632  r19.2zb  3682  ral0  3696  int0  4028  iun0  4111  0iun  4112  ord0eln0  4599  nlim0  4603  nsuceq0  4625  xp0r  4919  dm0  5046  dm0rn0  5049  reldm0  5050  elimasni  5194  cnv0  5238  co02  5346  dffv3  5687  fv01  5726  bropopvvv  6389  mpt20  6390  tz7.44-2  6628  0we1  6713  omordi  6772  omeulem1  6788  nnmordi  6837  omabs  6853  omsmolem  6859  0er  6903  omxpenlem  7172  cantnfle  7586  en3lp  7632  r1sdom  7660  r1pwss  7670  alephordi  7915  axdc3lem2  8291  zorn2lem7  8342  brdom3  8366  canthwe  8486  nlt1pi  8743  xrinfm0  10875  elixx3g  10889  elfz2  11010  om2uzlti  11249  hashf1lem2  11664  sum0  12474  fsumsplit  12492  sumsplit  12511  fsum2dlem  12513  sadc0  12925  sadcp1  12926  saddisjlem  12935  smu01lem  12956  smu01  12957  smu02  12958  prmreclem5  13247  vdwap0  13303  ram0  13349  0catg  13871  oduclatb  14530  0g0  14668  cntzrcl  15085  gexdvds  15177  gsumzsplit  15488  dprdcntz2  15555  00lss  15977  mplcoe1  16487  mplcoe2  16489  mplrcl  16509  strov2rcl  16590  00ply1bas  16593  0ntop  16937  haust1  17374  hauspwdom  17521  kqcldsat  17722  tsmssplit  18138  ustn0  18207  0met  18353  itg11  19540  itg0  19628  bddmulibl  19687  fsumharmonic  20807  ppiublem2  20944  lgsdir2lem3  21066  nbgra0edg  21401  uvtx01vtx  21458  eupath2lem1  21656  helloworld  21716  isarchi  24209  measvuni  24525  sibf0  24606  prod0  25226  fprod2dlem  25261  pw2f1ocnv  27002  dsmmbas2  27075  dsmmfi  27076  pmtrfrn  27272  psgnunilem5  27289  stoweidlem34  27654  2wlkonot3v  28076  2spthonot3v  28077  en3lpVD  28670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-dif 3287  df-nul 3593
  Copyright terms: Public domain W3C validator