Theorem sneqi 4584

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 4583	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐴} = {𝐵}

Syntax hints:   = wceq 1541  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-sn 4574

This theorem is referenced by:  fnressn  7091  fressnfv  7093  snriota  7336  xpassen  8984  ids1  14505  s3tpop  14816  bpoly3  15965  strle1  17069  2strop  17140  ghmeqker  19155  pws1  20243  pwsmgp  20245  lpival  21261  mat1dimelbas  22386  mat1dim0  22388  mat1dimid  22389  mat1dimscm  22390  mat1dimmul  22391  mat1f1o  22393  imasdsf1olem  24288  ehl0  25344  nosupcbv  27641  noinfcbv  27656  bday1s  27775  vtxval3sn  29021  iedgval3sn  29022  uspgr1v1eop  29227  hh0oi  31883  eulerpartlemmf  34388  bnj601  34932  dffv5  35966  zrdivrng  38003  isdrngo1  38006  aks5lem3a  42292  aks5lem7  42303  prjspval2  42716  mapfzcons  42819  mapfzcons1  42820  mapfzcons2  42822  df3o3  43417  fourierdlem80  46294  lmod1zr  48604  ovsng2  48969  setc1oterm  49602  setc1ohomfval  49604  setc1ocofval  49605  funcsetc1o  49608  termcfuncval  49643  termcnatval  49646