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

Theorem snidg 3831
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 2435 . 2  |-  A  =  A
2 elsncg 3828 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 225 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   {csn 3806
This theorem is referenced by:  snidb  3832  elsnc2g  3834  snnzg  3913  fvunsn  5916  fsnunfv  5924  1stconst  6426  2ndconst  6427  curry1  6429  curry2  6432  unifpw  7400  mapfien  7642  cfsuc  8126  eqs1  11749  swrds1  11775  ramub1lem1  13382  acsfiindd  14591  odf1o1  15194  gsumconst  15520  lspsolv  16203  maxlp  17199  cnpdis  17345  concompid  17482  dislly  17548  dfac14lem  17637  txtube  17660  pt1hmeo  17826  ufileu  17939  filufint  17940  uffix  17941  uffixsn  17945  i1fima2sn  19560  ply1rem  20074  1conngra  21650  vdgr1d  21662  vdgr1a  21665  eupap1  21686  esumel  24430  derangsn  24844  erdszelem4  24868  cvmlift2lem9  24986  locfindis  26322  neibastop2lem  26326  ismrer1  26484  kelac2  27078  rngunsnply  27293  en1uniel  27295  eldmressnsn  27900  funressnfv  27906  elpaddatriN  30439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sn 3812
  Copyright terms: Public domain W3C validator