Theorem sneqi 4612

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

Syntax hints:   = wceq 1540  {csn 4601

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-sn 4602

This theorem is referenced by:  fnressn  7148  fressnfv  7150  snriota  7395  xpassen  9080  ids1  14615  s3tpop  14928  bpoly3  16074  strle1  17177  2strop  17250  ghmeqker  19226  pws1  20285  pwsmgp  20287  lpival  21285  mat1dimelbas  22409  mat1dim0  22411  mat1dimid  22412  mat1dimscm  22413  mat1dimmul  22414  mat1f1o  22416  imasdsf1olem  24312  ehl0  25369  nosupcbv  27666  noinfcbv  27681  bday1s  27795  vtxval3sn  29022  iedgval3sn  29023  uspgr1v1eop  29228  hh0oi  31884  eulerpartlemmf  34407  bnj601  34951  dffv5  35942  zrdivrng  37977  isdrngo1  37980  aks5lem3a  42202  aks5lem7  42213  prjspval2  42636  mapfzcons  42739  mapfzcons1  42740  mapfzcons2  42742  df3o3  43338  fourierdlem80  46215  lmod1zr  48469  ovsng2  48835  setc1oterm  49376  setc1ohomfval  49378  setc1ocofval  49379  funcsetc1o  49382  termcfuncval  49417  termcnatval  49420