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

Theorem snidg 3994
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 2451 . 2  |-  A  =  A
2 elsncg 3991 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 237 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887   {csn 3968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-sn 3969
This theorem is referenced by:  snidb  3995  elsnc2g  3998  snnzg  4089  eldmressnsn  5144  elsnxp  5378  fvressn  6080  fsnunfv  6104  1stconst  6884  2ndconst  6885  curry1  6888  curry2  6891  suppsnop  6928  en1uniel  7641  unifpw  7877  sucprcreg  8114  cfsuc  8687  elfzomin  11985  hashrabsn1  12553  swrds1  12807  lcmfunsnlem1  14610  ramub1lem1  14984  acsfiindd  16423  mgm1  16500  mnd1OLD  16578  mnd1id  16579  odf1o1  17221  gsumconst  17567  lspsolv  18366  mat1ghm  19508  mat1mhm  19509  mavmul0  19577  m1detdiag  19622  mdetrlin  19627  mdetrsca  19628  chpmat1dlem  19859  maxlp  20163  cnpdis  20309  concompid  20446  dislly  20512  locfindis  20545  dfac14lem  20632  txtube  20655  pt1hmeo  20821  ufileu  20934  filufint  20935  uffix  20936  uffixsn  20940  i1fima2sn  22638  ply1rem  23114  1conngra  25403  vdgr1d  25631  vdgr1a  25634  eupap1  25704  esumel  28868  derangsn  29893  erdszelem4  29917  cvmlift2lem9  30034  fv1stcnv  30422  fv2ndcnv  30423  neibastop2lem  31016  bj-sels  31556  ismrer1  32170  elpaddatriN  33368  kelac2  35923  rngunsnply  36039  brtrclfv2  36319  projf1o  37474  mapsnd  37476  mccllem  37677  limcresiooub  37723  limcresioolb  37724  cnfdmsn  37759  cxpcncf2  37778  dvmptfprodlem  37819  dvnprodlem1  37821  dvnprodlem2  37822  dvnprodlem3  37823  fourierdlem49  38019  prsal  38179  salexct  38193  salgencntex  38202  sge0sn  38221  sge0snmpt  38225  sge0snmptf  38279  caratheodorylem1  38347  hoiprodp1  38410  hoidmv1le  38416  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvlelem4  38420  hspmbllem2  38449  funressnfv  38629  el1fzopredsuc  38722  uhgrvd0nedgb  39545  uspgrloopvd2  39557  snlindsntor  40317  lmod1lem1  40333  lmod1lem2  40334  lmod1lem3  40335  lmod1lem4  40336  lmod1lem5  40337  lmod1zr  40339
  Copyright terms: Public domain W3C validator