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

Theorem snidg 4053
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
Assertion
Ref Expression
snidg  |-  ( A  e.  V  ->  A  e.  { A } )

Proof of Theorem snidg
StepHypRef Expression
1 eqid 2467 . 2  |-  A  =  A
2 elsncg 4050 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-sn 4028
This theorem is referenced by:  snidb  4054  elsnc2g  4057  snnzg  4144  eldmressnsn  5311  fvressn  6075  fvunsn  6091  fsnunfv  6099  1stconst  6868  2ndconst  6869  curry1  6872  curry2  6875  suppsnop  6912  en1uniel  7584  unifpw  7819  sucprcreg  8021  mapfienOLD  8134  cfsuc  8633  elfzomin  11851  hashrabsn1  12406  eqs1  12580  swrds1  12635  ramub1lem1  14399  acsfiindd  15660  odf1o1  16388  gsumconst  16745  lspsolv  17572  mat1ghm  18752  mat1mhm  18753  mavmul0  18821  m1detdiag  18866  mdetrlin  18871  mdetrsca  18872  chpmat1dlem  19103  maxlp  19414  cnpdis  19560  concompid  19698  dislly  19764  dfac14lem  19853  txtube  19876  pt1hmeo  20042  ufileu  20155  filufint  20156  uffix  20157  uffixsn  20161  i1fima2sn  21822  ply1rem  22299  1conngra  24351  vdgr1d  24579  vdgr1a  24582  eupap1  24652  esumel  27698  derangsn  28254  erdszelem4  28278  cvmlift2lem9  28396  locfindis  29777  neibastop2lem  29781  ismrer1  29937  kelac2  30615  rngunsnply  30727  limcresiooub  31184  limcresioolb  31185  cnfdmsn  31220  fourierdlem49  31456  funressnfv  31680  snlindsntor  32145  mnd1  32161  grp1  32162  lmod1lem1  32169  lmod1lem2  32170  lmod1lem3  32171  lmod1lem4  32172  lmod1lem5  32173  lmod1zr  32175  bj-sels  33601  elpaddatriN  34599
  Copyright terms: Public domain W3C validator