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

Theorem noel 3632
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 3469 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3470 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3629 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2500 . 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 1725   _Vcvv 2956    \ cdif 3317   (/)c0 3628
This theorem is referenced by:  n0i  3633  n0f  3636  rex0  3641  abvor0  3645  rab0  3648  un0  3652  in0  3653  0ss  3656  disj  3668  r19.2zb  3718  ral0  3732  int0  4064  iun0  4147  0iun  4148  ord0eln0  4635  nlim0  4639  nsuceq0  4661  xp0r  4956  dm0  5083  dm0rn0  5086  reldm0  5087  elimasni  5231  cnv0  5275  co02  5383  dffv3  5724  fv01  5763  bropopvvv  6426  mpt20  6427  tz7.44-2  6665  0we1  6750  omordi  6809  omeulem1  6825  nnmordi  6874  omabs  6890  omsmolem  6896  0er  6940  omxpenlem  7209  cantnfle  7626  en3lp  7672  r1sdom  7700  r1pwss  7710  alephordi  7955  axdc3lem2  8331  zorn2lem7  8382  brdom3  8406  canthwe  8526  nlt1pi  8783  xrinfm0  10915  elixx3g  10929  elfz2  11050  om2uzlti  11290  hashf1lem2  11705  sum0  12515  fsumsplit  12533  sumsplit  12552  fsum2dlem  12554  sadc0  12966  sadcp1  12967  saddisjlem  12976  smu01lem  12997  smu01  12998  smu02  12999  prmreclem5  13288  vdwap0  13344  ram0  13390  0catg  13912  oduclatb  14571  0g0  14709  cntzrcl  15126  gexdvds  15218  gsumzsplit  15529  dprdcntz2  15596  00lss  16018  mplcoe1  16528  mplcoe2  16530  mplrcl  16550  strov2rcl  16631  00ply1bas  16634  0ntop  16978  haust1  17416  hauspwdom  17564  kqcldsat  17765  tsmssplit  18181  ustn0  18250  0met  18396  itg11  19583  itg0  19671  bddmulibl  19730  fsumharmonic  20850  ppiublem2  20987  lgsdir2lem3  21109  nbgra0edg  21444  uvtx01vtx  21501  eupath2lem1  21699  helloworld  21759  isarchi  24252  measvuni  24568  sibf0  24649  prod0  25269  fprod2dlem  25304  opelco3  25403  wsuclem  25576  pw2f1ocnv  27108  dsmmbas2  27180  dsmmfi  27181  pmtrfrn  27377  psgnunilem5  27394  stoweidlem34  27759  2wlkonot3v  28342  2spthonot3v  28343  en3lpVD  28957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-dif 3323  df-nul 3629
  Copyright terms: Public domain W3C validator