Theorem sneqi 4569

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

Syntax hints:   = wceq 1548  {csn 4558

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 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-sn 4559

This theorem is referenced by:  fnressn  7105  fressnfv  7107  snriota  7350  xpassen  9003  ids1  14555  s3tpop  14866  bpoly3  16018  strle1  17123  2strop  17194  ghmeqker  19213  pws1  20299  pwsmgp  20301  lpival  21321  mat1dimelbas  22458  mat1dim0  22460  mat1dimid  22461  mat1dimscm  22462  mat1dimmul  22463  mat1f1o  22465  imasdsf1olem  24360  ehl0  25406  nosupcbv  27688  noinfcbv  27703  bday1  27828  bdaypw2n0bndlem  28477  vtxval3sn  29134  iedgval3sn  29135  uspgr1v1eop  29340  hh0oi  31996  selvply1rhm0  33722  eulerpartlemmf  34571  bnj601  35117  dffv5  36165  zrdivrng  38335  isdrngo1  38338  aks5lem3a  42689  aks5lem7  42700  prjspval2  43078  mapfzcons  43180  mapfzcons1  43181  mapfzcons2  43183  df3o3  43774  fourierdlem80  46643  lmod1zr  48998  ovsng2  49363  setc1oterm  49995  setc1ohomfval  49997  setc1ocofval  49998  funcsetc1o  50001  termcfuncval  50036  termcnatval  50039