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

Theorem snidg 4028
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 2429 . 2  |-  A  =  A
2 elsncg 4025 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 236 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870   {csn 4002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-sn 4003
This theorem is referenced by:  snidb  4029  elsnc2g  4032  snnzg  4120  eldmressnsn  5164  fvressn  6095  fsnunfv  6119  1stconst  6895  2ndconst  6896  curry1  6899  curry2  6902  suppsnop  6939  en1uniel  7648  unifpw  7883  sucprcreg  8114  cfsuc  8685  elfzomin  11982  hashrabsn1  12550  swrds1  12792  lcmfunsnlem1  14581  ramub1lem1  14947  acsfiindd  16374  mgm1  16451  mnd1OLD  16529  mnd1id  16530  odf1o1  17159  gsumconst  17502  lspsolv  18301  mat1ghm  19439  mat1mhm  19440  mavmul0  19508  m1detdiag  19553  mdetrlin  19558  mdetrsca  19559  chpmat1dlem  19790  maxlp  20094  cnpdis  20240  concompid  20377  dislly  20443  locfindis  20476  dfac14lem  20563  txtube  20586  pt1hmeo  20752  ufileu  20865  filufint  20866  uffix  20867  uffixsn  20871  i1fima2sn  22515  ply1rem  22989  1conngra  25248  vdgr1d  25476  vdgr1a  25479  eupap1  25549  elsnxp  28063  esumel  28707  derangsn  29681  erdszelem4  29705  cvmlift2lem9  29822  fv1stcnv  30209  fv2ndcnv  30210  neibastop2lem  30801  bj-sels  31305  ismrer1  31877  elpaddatriN  33080  kelac2  35632  rngunsnply  35741  brtrclfv2  35961  mccllem  37252  limcresiooub  37298  limcresioolb  37299  cnfdmsn  37334  cxpcncf2  37353  dvmptfprodlem  37391  dvnprodlem1  37393  dvnprodlem2  37394  dvnprodlem3  37395  fourierdlem49  37590  prsal  37729  sge0sn  37758  sge0snmpt  37762  caratheodorylem1  37859  funressnfv  38032  el1fzopredsuc  38124  snlindsntor  39036  lmod1lem1  39052  lmod1lem2  39053  lmod1lem3  39054  lmod1lem4  39055  lmod1lem5  39056  lmod1zr  39058
  Copyright terms: Public domain W3C validator