Theorem sneqi 4605

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

Syntax hints:   = wceq 1567  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-sn 4595

This theorem is referenced by:  fnressn  7156  fressnfv  7158  snriota  7401  xpassen  9059  ids1  14635  s3tpop  14946  bpoly3  16112  strle1  17218  2strop  17289  ghmeqker  19313  pws1  20406  pwsmgp  20408  lpival  21461  mat1dimelbas  22597  mat1dim0  22599  mat1dimid  22600  mat1dimscm  22601  mat1dimmul  22602  mat1f1o  22604  imasdsf1olem  24499  ehl0  25545  nosupcbv  27832  noinfcbv  27847  bday1  27973  bdaypw2n0bndlem  28622  vtxval3sn  29334  iedgval3sn  29335  uspgr1v1eop  29540  hh0oi  32196  selvply1rhm0  33861  eulerpartlemmf  34710  bnj601  35253  dffv5  36313  zrdivrng  38492  isdrngo1  38495  aks5lem3a  42846  aks5lem7  42857  prjspval2  43237  mapfzcons  43339  mapfzcons1  43340  mapfzcons2  43342  df3o3  43933  fourierdlem80  46792  isprmrng  48990  lmod1zr  49158  ovsng2  49522  setc1oterm  50154  setc1ohomfval  50156  setc1ocofval  50157  funcsetc1o  50160  termcfuncval  50195  termcnatval  50198