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

Theorem noel 3401
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 3240 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3241 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 167 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3398 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2320 . 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 2740    \ cdif 3091   (/)c0 3397
This theorem is referenced by:  n0i  3402  n0f  3405  rex0  3410  abvor0  3414  rab0  3417  un0  3421  in0  3422  0ss  3425  disj  3437  r19.2zb  3486  ral0  3500  int0  3817  iun0  3899  0iun  3900  ord0eln0  4383  nlim0  4387  nsuceq0  4409  xp0r  4721  dm0  4845  dm0rn0  4848  reldm0  4849  elimasni  4993  cnv0  5037  co02  5138  fv01  5458  mpt20  6098  tz7.44-2  6353  0we1  6438  omordi  6497  omeulem1  6513  nnmordi  6562  omabs  6578  omsmolem  6584  0er  6628  omxpenlem  6896  cantnfle  7305  en3lp  7351  r1sdom  7379  r1pwss  7389  alephordi  7634  axdc3lem2  8010  zorn2lem7  8062  brdom3  8086  canthwe  8206  nlt1pi  8463  xrinfm0  10586  elixx3g  10600  elfz2  10720  om2uzlti  10944  hashf1lem2  11324  sum0  12124  fsumsplit  12142  sumsplit  12161  fsum2dlem  12163  sadc0  12572  sadcp1  12573  saddisjlem  12582  smu01lem  12603  smu01  12604  smu02  12605  prmreclem5  12894  vdwap0  12950  ram0  12996  0catg  13516  oduclatb  14175  0g0  14313  cntzrcl  14730  gexdvds  14822  gsumzsplit  15133  dprdcntz2  15200  00lss  15626  mplcoe1  16136  mplcoe2  16138  mplrcl  16158  strov2rcl  16242  00ply1bas  16245  0ntop  16578  haust1  17007  hauspwdom  17154  kqcldsat  17351  tsmssplit  17761  0met  17857  itg11  18973  itg0  19061  bddmulibl  19120  fsumharmonic  20232  ppiublem2  20369  lgsdir2lem3  20491  helloworld  20763  eupath2lem1  23238  funpartfv  23823  elioo1t3  24834  0ded  25089  0catOLD  25090  pw2f1ocnv  26462  dsmmbas2  26535  dsmmfi  26536  pmtrfrn  26732  psgnunilem5  26749  stoweidlem34  27083  en3lpVD  27634
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-dif 3097  df-nul 3398
  Copyright terms: Public domain W3C validator