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

Theorem snidg 4584
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 2824 . 2 𝐴 = 𝐴
2 elsng 4564 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 261 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  {csn 4550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-sn 4551
This theorem is referenced by:  snidb  4585  elsn2g  4588  elinsn  4631  snnzg  4695  sneqrg  4754  sels  5321  eldmressnsn  5882  elsnxp  6129  fvressn  6915  fvsnun1  6935  fsnunfv  6940  1stconst  7791  2ndconst  7792  curry1  7795  curry2  7798  suppsnop  7840  mapsnd  8446  en1uniel  8577  unifpw  8824  sucprcreg  9062  djurf1o  9339  cfsuc  9677  elfzomin  13113  hashrabsn1  13740  swrds1  14028  fsumsplitsnun  15110  lcmfunsnlem1  15979  ramub1lem1  16360  basprssdmsets  16549  acsfiindd  17787  mgm1  17868  mnd1id  17953  odf1o1  18697  gsumconst  19054  lspsolv  19915  mat1ghm  21092  mat1mhm  21093  mavmul0  21161  m1detdiag  21206  mdetrlin  21211  mdetrsca  21212  chpmat1dlem  21443  maxlp  21755  cnpdis  21901  conncompid  22039  dislly  22105  locfindis  22138  dfac14lem  22225  txtube  22248  pt1hmeo  22414  ufileu  22527  filufint  22528  uffix  22529  uffixsn  22533  i1fima2sn  24287  ply1rem  24767  edglnl  26939  vtxd0nedgb  27281  1loopgrvd2  27296  wlkp1  27474  1wlkdlem2  27926  1conngr  27982  frgrwopregasn  28104  frgrwopregbsn  28105  wlkl0  28155  esumel  31363  actfunsnrndisj  31933  reprsuc  31943  breprexplema  31958  derangsn  32474  erdszelem4  32498  cvmlift2lem9  32615  fv1stcnv  33077  fv2ndcnv  33078  noextenddif  33232  noextendlt  33233  noextendgt  33234  neibastop2lem  33765  bj-nsnid  34430  bj-snmoore  34473  ismrer1  35221  elpaddatriN  37044  fnsnbt  39348  frlmsnic  39387  kelac2  39925  rngunsnply  40033  brtrclfv2  40344  k0004lem3  40771  projf1o  41750  fsneq  41760  fsneqrn  41765  unirnmapsn  41768  ssmapsn  41770  fconst7  41830  mccllem  42165  limcresiooub  42210  limcresioolb  42211  cnfdmsn  42450  cxpcncf2  42467  dvmptfprodlem  42512  dvnprodlem1  42514  dvnprodlem2  42515  dvnprodlem3  42516  fourierdlem49  42723  prsal  42886  salexct  42900  salgencntex  42909  sge0sn  42944  sge0snmpt  42948  sge0snmptf  43002  caratheodorylem1  43091  hoiprodp1  43153  hoidmv1le  43159  hoidmvlelem1  43160  hoidmvlelem2  43161  hoidmvlelem3  43162  hoidmvlelem4  43163  hspmbllem2  43192  ovnovollem1  43221  ovnovollem2  43222  funressnfv  43561  el1fzopredsuc  43808  snlindsntor  44806  lmod1lem1  44822  lmod1lem2  44823  lmod1lem3  44824  lmod1lem4  44825  lmod1lem5  44826  lmod1zr  44828
  Copyright terms: Public domain W3C validator