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

Theorem snidg 3625
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 2256 . 2  |-  A  =  A
2 elsncg 3622 . 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 3600
This theorem is referenced by:  snidb  3626  elsnc2g  3628  snnzg  3703  fvunsn  5632  fsnunf2  5639  fsnunfv  5640  1stconst  6127  2ndconst  6128  curry1  6130  curry2  6133  unifpw  7112  mapfien  7353  cfsuc  7837  eqs1  11398  swrds1  11424  rpnnen2lem9  12449  ramub1lem1  13021  ramub1lem2  13022  acsfiindd  14228  odf1o1  14831  gsumconst  15157  lspsolv  15844  maxlp  16826  cnpdis  16969  concompid  17105  dislly  17171  dfac14lem  17259  txtube  17282  pt1hmeo  17445  ufileu  17562  filufint  17563  uffix  17564  uffixsn  17568  i1fima2sn  18983  ply1rem  19497  derangsn  23059  erdszelem4  23083  cvmlift2lem9  23200  vdgr1d  23252  vdgr1a  23255  eupap1  23258  cbicp  24519  fnckle  25398  lineval2a  25438  sgplpte21d1  25492  locfindis  25658  neibastop2lem  25662  ismrer1  25915  prtlem80  26077  kelac2  26516  rngunsnply  26731  en1uniel  26733  elpaddatriN  29143
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 2759  df-sn 3606
  Copyright terms: Public domain W3C validator