Theorem sneqi 4637

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

Syntax hints:   = wceq 1540  {csn 4626

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-sn 4627

This theorem is referenced by:  fnressn  7178  fressnfv  7180  snriota  7421  xpassen  9106  ids1  14635  s3tpop  14948  bpoly3  16094  strle1  17195  2strop1  17273  ghmeqker  19261  pws1  20322  pwsmgp  20324  lpival  21334  mat1dimelbas  22477  mat1dim0  22479  mat1dimid  22480  mat1dimscm  22481  mat1dimmul  22482  mat1f1o  22484  imasdsf1olem  24383  ehl0  25451  nosupcbv  27747  noinfcbv  27762  bday1s  27876  cutpw2  28417  pw2bday  28418  vtxval3sn  29060  iedgval3sn  29061  uspgr1v1eop  29266  hh0oi  31922  eulerpartlemmf  34377  bnj601  34934  dffv5  35925  zrdivrng  37960  isdrngo1  37963  aks5lem3a  42190  aks5lem7  42201  prjspval2  42623  mapfzcons  42727  mapfzcons1  42728  mapfzcons2  42730  df3o3  43327  fourierdlem80  46201  lmod1zr  48410  setc1oterm  49134  mndtchom  49181