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

Theorem snidg 4625
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 (𝐴𝑉𝐴 ∈ {𝐴})

Proof of Theorem snidg
StepHypRef Expression
1 eqid 2737 . 2 𝐴 = 𝐴
2 elsng 4605 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 258 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-sn 4592
This theorem is referenced by:  snidb  4626  elsn2g  4629  elinsn  4676  snnzg  4740  sneqrg  4802  selsALT  5401  intidg  5419  eldmressnsn  5985  elsnxp  6248  fvressn  7113  fvsnun1  7133  fsnunfv  7138  1stconst  8037  2ndconst  8038  curry1  8041  curry2  8044  suppsnop  8114  mapsnd  8831  en1uniel  8979  en1unielOLD  8980  dif1enlem  9107  dif1enlemOLD  9108  unifpw  9306  sucprcreg  9544  djurf1o  9856  cfsuc  10200  elfzomin  13651  hashrabsn1  14281  swrds1  14561  fsumsplitsnun  15647  lcmfunsnlem1  16520  ramub1lem1  16905  basprssdmsets  17103  acsfiindd  18449  mgm1  18520  mnd1id  18605  odf1o1  19361  gsumconst  19718  lspsolv  20620  mat1ghm  21848  mat1mhm  21849  mavmul0  21917  m1detdiag  21962  mdetrlin  21967  mdetrsca  21968  chpmat1dlem  22200  maxlp  22514  cnpdis  22660  conncompid  22798  dislly  22864  locfindis  22897  dfac14lem  22984  txtube  23007  pt1hmeo  23173  ufileu  23286  filufint  23287  uffix  23288  uffixsn  23292  i1fima2sn  25060  ply1rem  25544  noextenddif  27032  noextendlt  27033  noextendgt  27034  addsval  27296  negsunif  27372  mulsval  27396  mulsproplem6  27406  mulsproplem7  27407  mulsproplem8  27408  mulsproplem9  27409  edglnl  28136  vtxd0nedgb  28478  1loopgrvd2  28493  wlkp1  28671  1wlkdlem2  29124  1conngr  29180  frgrwopregasn  29302  frgrwopregbsn  29303  wlkl0  29353  esumel  32686  actfunsnrndisj  33258  reprsuc  33268  breprexplema  33283  derangsn  33804  erdszelem4  33828  cvmlift2lem9  33945  fv1stcnv  34390  fv2ndcnv  34391  neibastop2lem  34861  bj-nsnid  35570  bj-snmoore  35613  ismrer1  36326  elpaddatriN  38295  fnsnbt  40686  frlmsnic  40757  kelac2  41421  rngunsnply  41529  brtrclfv2  42073  k0004lem3  42495  projf1o  43491  fsneq  43501  fsneqrn  43506  unirnmapsn  43509  ssmapsn  43511  fconst7  43567  mccllem  43912  limcresiooub  43957  limcresioolb  43958  cnfdmsn  44197  cxpcncf2  44214  dvmptfprodlem  44259  dvnprodlem1  44261  dvnprodlem2  44262  dvnprodlem3  44263  fourierdlem49  44470  prsal  44633  salexct  44649  salgencntex  44658  sge0sn  44694  sge0snmpt  44698  sge0snmptf  44752  caratheodorylem1  44841  hoiprodp1  44903  hoidmv1le  44909  hoidmvlelem1  44910  hoidmvlelem2  44911  hoidmvlelem3  44912  hoidmvlelem4  44913  hspmbllem2  44942  ovnovollem1  44971  ovnovollem2  44972  funressnfv  45351  cfsetsnfsetf  45366  cfsetsnfsetfo  45368  el1fzopredsuc  45631  snlindsntor  46626  lmod1lem1  46642  lmod1lem2  46643  lmod1lem3  46644  lmod1lem4  46645  lmod1lem5  46646  lmod1zr  46648
  Copyright terms: Public domain W3C validator