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

Theorem snidg 3569
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 2253 . 2  |-  A  =  A
2 elsncg 3566 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 226 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   {csn 3544
This theorem is referenced by:  snidb  3570  elsnc2g  3572  snnzg  3647  fvunsn  5564  fsnunf2  5571  fsnunfv  5572  1stconst  6059  2ndconst  6060  curry1  6062  curry2  6065  unifpw  7042  mapfien  7283  cfsuc  7767  eqs1  11324  swrds1  11350  rpnnen2lem9  12375  ramub1lem1  12947  ramub1lem2  12948  odf1o1  14718  gsumconst  15044  lspsolv  15731  maxlp  16710  cnpdis  16853  concompid  16989  dislly  17055  dfac14lem  17143  txtube  17166  pt1hmeo  17329  ufileu  17446  filufint  17447  uffix  17448  uffixsn  17452  i1fima2sn  18867  ply1rem  19381  derangsn  22872  erdszelem4  22896  cvmlift2lem9  23013  vdgr1d  23065  vdgr1a  23068  eupap1  23071  cbicp  24332  fnckle  25211  lineval2a  25251  sgplpte21d1  25305  locfindis  25471  neibastop2lem  25475  ismrer1  25728  prtlem80  25890  kelac2  26329  rngunsnply  26544  en1uniel  26546  elpaddatriN  28896
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-sn 3550
  Copyright terms: Public domain W3C validator