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

Theorem snidg 3666
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 2284 . 2  |-  A  =  A
2 elsncg 3663 . 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 1628    e. wcel 1688   {csn 3641
This theorem is referenced by:  snidb  3667  elsnc2g  3669  snnzg  3744  fvunsn  5673  fsnunf2  5680  fsnunfv  5681  1stconst  6168  2ndconst  6169  curry1  6171  curry2  6174  unifpw  7153  mapfien  7394  cfsuc  7878  eqs1  11441  swrds1  11467  rpnnen2lem9  12495  ramub1lem1  13067  ramub1lem2  13068  acsfiindd  14274  odf1o1  14877  gsumconst  15203  lspsolv  15890  maxlp  16872  cnpdis  17015  concompid  17151  dislly  17217  dfac14lem  17305  txtube  17328  pt1hmeo  17491  ufileu  17608  filufint  17609  uffix  17610  uffixsn  17614  i1fima2sn  19029  ply1rem  19543  derangsn  23105  erdszelem4  23129  cvmlift2lem9  23246  vdgr1d  23298  vdgr1a  23301  eupap1  23304  cbicp  24565  fnckle  25444  lineval2a  25484  sgplpte21d1  25538  locfindis  25704  neibastop2lem  25708  ismrer1  25961  prtlem80  26123  kelac2  26562  rngunsnply  26777  en1uniel  26779  eldmressnsn  27357  funressnfv  27364  elpaddatriN  29259
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-sn 3647
  Copyright terms: Public domain W3C validator