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

Theorem snidg 3918
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 2443 . 2  |-  A  =  A
2 elsncg 3915 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   {csn 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2989  df-sn 3893
This theorem is referenced by:  snidb  3919  elsnc2g  3922  snnzg  4007  fvunsn  5925  fsnunfv  5933  1stconst  6676  2ndconst  6677  curry1  6679  curry2  6682  suppsnop  6719  en1uniel  7396  unifpw  7629  sucprcreg  7829  mapfienOLD  7942  cfsuc  8441  elfzomin  11622  eqs1  12315  swrds1  12360  ramub1lem1  14102  acsfiindd  15362  odf1o1  16086  gsumconst  16442  lspsolv  17239  mavmul0  18378  mdetrlin  18424  mdetrsca  18425  maxlp  18766  cnpdis  18912  concompid  19050  dislly  19116  dfac14lem  19205  txtube  19228  pt1hmeo  19394  ufileu  19507  filufint  19508  uffix  19509  uffixsn  19513  i1fima2sn  21173  ply1rem  21650  1conngra  23576  vdgr1d  23588  vdgr1a  23591  eupap1  23612  esumel  26516  derangsn  27073  erdszelem4  27097  cvmlift2lem9  27215  locfindis  28596  neibastop2lem  28600  ismrer1  28756  kelac2  29437  rngunsnply  29549  eldmressnsn  30048  funressnfv  30053  fvressn  30171  hashrabsn1  30252  m1detdiag  30953  snlindsntor  31024  mnd1  31040  grp1  31041  lmod1lem1  31048  lmod1lem2  31049  lmod1lem3  31050  lmod1lem4  31051  lmod1lem5  31052  lmod1zr  31054  bj-sels  32474  elpaddatriN  33466
  Copyright terms: Public domain W3C validator