Theorem sneqi 4596

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

Syntax hints:   = wceq 1540  {csn 4585

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 4586

This theorem is referenced by:  fnressn  7112  fressnfv  7114  snriota  7359  xpassen  9012  ids1  14538  s3tpop  14851  bpoly3  16000  strle1  17104  2strop  17175  ghmeqker  19157  pws1  20245  pwsmgp  20247  lpival  21266  mat1dimelbas  22391  mat1dim0  22393  mat1dimid  22394  mat1dimscm  22395  mat1dimmul  22396  mat1f1o  22398  imasdsf1olem  24294  ehl0  25350  nosupcbv  27647  noinfcbv  27662  bday1s  27780  vtxval3sn  29023  iedgval3sn  29024  uspgr1v1eop  29229  hh0oi  31882  eulerpartlemmf  34359  bnj601  34903  dffv5  35905  zrdivrng  37940  isdrngo1  37943  aks5lem3a  42170  aks5lem7  42181  prjspval2  42594  mapfzcons  42697  mapfzcons1  42698  mapfzcons2  42700  df3o3  43296  fourierdlem80  46177  lmod1zr  48475  ovsng2  48840  setc1oterm  49473  setc1ohomfval  49475  setc1ocofval  49476  funcsetc1o  49479  termcfuncval  49514  termcnatval  49517