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

Theorem snidg 4042
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 2454 . 2  |-  A  =  A
2 elsncg 4039 . 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 1398    e. wcel 1823   {csn 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-sn 4017
This theorem is referenced by:  snidb  4043  elsnc2g  4046  snnzg  4133  eldmressnsn  5301  fvressn  6063  fsnunfv  6087  1stconst  6861  2ndconst  6862  curry1  6865  curry2  6868  suppsnop  6905  en1uniel  7580  unifpw  7815  sucprcreg  8017  mapfienOLD  8129  cfsuc  8628  elfzomin  11868  hashrabsn1  12425  swrds1  12667  ramub1lem1  14628  acsfiindd  16006  mgm1  16083  mnd1OLD  16161  mnd1id  16162  odf1o1  16791  gsumconst  17152  lspsolv  17984  mat1ghm  19152  mat1mhm  19153  mavmul0  19221  m1detdiag  19266  mdetrlin  19271  mdetrsca  19272  chpmat1dlem  19503  maxlp  19815  cnpdis  19961  concompid  20098  dislly  20164  locfindis  20197  dfac14lem  20284  txtube  20307  pt1hmeo  20473  ufileu  20586  filufint  20587  uffix  20588  uffixsn  20592  i1fima2sn  22253  ply1rem  22730  1conngra  24877  vdgr1d  25105  vdgr1a  25108  eupap1  25178  elsnxp  27684  esumel  28276  derangsn  28878  erdszelem4  28902  cvmlift2lem9  29020  neibastop2lem  30418  ismrer1  30574  kelac2  31250  rngunsnply  31363  mccllem  31844  limcresiooub  31887  limcresioolb  31888  cnfdmsn  31923  cxpcncf2  31942  dvmptfprodlem  31980  dvnprodlem1  31982  dvnprodlem2  31983  dvnprodlem3  31984  fourierdlem49  32177  funressnfv  32452  snlindsntor  33326  lmod1lem1  33342  lmod1lem2  33343  lmod1lem3  33344  lmod1lem4  33345  lmod1lem5  33346  lmod1zr  33348  bj-sels  34921  elpaddatriN  35924
  Copyright terms: Public domain W3C validator