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

Theorem snidg 3665
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 2283 . 2  |-  A  =  A
2 elsncg 3662 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 224 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {csn 3640
This theorem is referenced by:  snidb  3666  elsnc2g  3668  snnzg  3743  fvunsn  5712  fsnunf2  5719  fsnunfv  5720  1stconst  6207  2ndconst  6208  curry1  6210  curry2  6213  unifpw  7158  mapfien  7399  cfsuc  7883  eqs1  11447  swrds1  11473  rpnnen2lem9  12501  ramub1lem1  13073  ramub1lem2  13074  acsfiindd  14280  odf1o1  14883  gsumconst  15209  lspsolv  15896  maxlp  16878  cnpdis  17021  concompid  17157  dislly  17223  dfac14lem  17311  txtube  17334  pt1hmeo  17497  ufileu  17614  filufint  17615  uffix  17616  uffixsn  17620  i1fima2sn  19035  ply1rem  19549  esumel  23426  derangsn  23701  erdszelem4  23725  cvmlift2lem9  23842  vdgr1d  23894  vdgr1a  23897  eupap1  23900  cbicp  25166  fnckle  26045  lineval2a  26085  sgplpte21d1  26139  locfindis  26305  neibastop2lem  26309  ismrer1  26562  prtlem80  26724  kelac2  27163  rngunsnply  27378  en1uniel  27380  eldmressnsn  27984  funressnfv  27991  elpaddatriN  29992
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
  Copyright terms: Public domain W3C validator