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

Theorem snidg 4590
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 2738 . 2 𝐴 = 𝐴
2 elsng 4570 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 261 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2111  {csn 4556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4557
This theorem is referenced by:  snidb  4591  elsn2g  4594  elinsn  4641  snnzg  4705  sneqrg  4765  sels  5341  eldmressnsn  5909  elsnxp  6169  fvressn  6996  fvsnun1  7016  fsnunfv  7021  1stconst  7887  2ndconst  7888  curry1  7891  curry2  7894  suppsnop  7941  mapsnd  8588  en1uniel  8728  en1unielOLD  8729  dif1enlem  8861  unifpw  9004  sucprcreg  9242  djurf1o  9554  cfsuc  9896  elfzomin  13339  hashrabsn1  13966  swrds1  14256  fsumsplitsnun  15344  lcmfunsnlem1  16219  ramub1lem1  16604  basprssdmsets  16797  acsfiindd  18084  mgm1  18155  mnd1id  18240  odf1o1  18986  gsumconst  19344  lspsolv  20205  mat1ghm  21404  mat1mhm  21405  mavmul0  21473  m1detdiag  21518  mdetrlin  21523  mdetrsca  21524  chpmat1dlem  21756  maxlp  22068  cnpdis  22214  conncompid  22352  dislly  22418  locfindis  22451  dfac14lem  22538  txtube  22561  pt1hmeo  22727  ufileu  22840  filufint  22841  uffix  22842  uffixsn  22846  i1fima2sn  24601  ply1rem  25085  edglnl  27258  vtxd0nedgb  27600  1loopgrvd2  27615  wlkp1  27793  1wlkdlem2  28245  1conngr  28301  frgrwopregasn  28423  frgrwopregbsn  28424  wlkl0  28474  esumel  31751  actfunsnrndisj  32321  reprsuc  32331  breprexplema  32346  derangsn  32868  erdszelem4  32892  cvmlift2lem9  33009  fv1stcnv  33493  fv2ndcnv  33494  noextenddif  33634  noextendlt  33635  noextendgt  33636  addsval  33889  neibastop2lem  34312  bj-nsnid  35003  bj-snmoore  35046  ismrer1  35760  elpaddatriN  37581  fnsnbt  39950  frlmsnic  40004  kelac2  40622  rngunsnply  40730  brtrclfv2  41041  k0004lem3  41465  projf1o  42438  fsneq  42448  fsneqrn  42453  unirnmapsn  42456  ssmapsn  42458  fconst7  42513  mccllem  42842  limcresiooub  42887  limcresioolb  42888  cnfdmsn  43127  cxpcncf2  43144  dvmptfprodlem  43189  dvnprodlem1  43191  dvnprodlem2  43192  dvnprodlem3  43193  fourierdlem49  43400  prsal  43563  salexct  43577  salgencntex  43586  sge0sn  43621  sge0snmpt  43625  sge0snmptf  43679  caratheodorylem1  43768  hoiprodp1  43830  hoidmv1le  43836  hoidmvlelem1  43837  hoidmvlelem2  43838  hoidmvlelem3  43839  hoidmvlelem4  43840  hspmbllem2  43869  ovnovollem1  43898  ovnovollem2  43899  funressnfv  44238  cfsetsnfsetf  44253  cfsetsnfsetfo  44255  el1fzopredsuc  44519  snlindsntor  45514  lmod1lem1  45530  lmod1lem2  45531  lmod1lem3  45532  lmod1lem4  45533  lmod1lem5  45534  lmod1zr  45536
  Copyright terms: Public domain W3C validator