Theorem sneqi 4588

Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sneqi	⊢ {𝐴} = {𝐵}

Proof of Theorem sneqi

Step	Hyp	Ref	Expression
1		sneqi.1	. 2 ⊢ 𝐴 = 𝐵
2		sneq 4587	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐴} = {𝐵}

Syntax hints:   = wceq 1540  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4578

This theorem is referenced by:  fnressn  7092  fressnfv  7094  snriota  7339  xpassen  8988  ids1  14504  s3tpop  14816  bpoly3  15965  strle1  17069  2strop  17140  ghmeqker  19122  pws1  20210  pwsmgp  20212  lpival  21231  mat1dimelbas  22356  mat1dim0  22358  mat1dimid  22359  mat1dimscm  22360  mat1dimmul  22361  mat1f1o  22363  imasdsf1olem  24259  ehl0  25315  nosupcbv  27612  noinfcbv  27627  bday1s  27745  vtxval3sn  28988  iedgval3sn  28989  uspgr1v1eop  29194  hh0oi  31847  eulerpartlemmf  34343  bnj601  34887  dffv5  35902  zrdivrng  37937  isdrngo1  37940  aks5lem3a  42166  aks5lem7  42177  prjspval2  42590  mapfzcons  42693  mapfzcons1  42694  mapfzcons2  42696  df3o3  43291  fourierdlem80  46171  lmod1zr  48482  ovsng2  48847  setc1oterm  49480  setc1ohomfval  49482  setc1ocofval  49483  funcsetc1o  49486  termcfuncval  49521  termcnatval  49524