Theorem sneqi 4603

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

Syntax hints:   = wceq 1540  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-sn 4593

This theorem is referenced by:  fnressn  7133  fressnfv  7135  snriota  7380  xpassen  9040  ids1  14569  s3tpop  14882  bpoly3  16031  strle1  17135  2strop  17206  ghmeqker  19182  pws1  20241  pwsmgp  20243  lpival  21241  mat1dimelbas  22365  mat1dim0  22367  mat1dimid  22368  mat1dimscm  22369  mat1dimmul  22370  mat1f1o  22372  imasdsf1olem  24268  ehl0  25324  nosupcbv  27621  noinfcbv  27636  bday1s  27750  vtxval3sn  28977  iedgval3sn  28978  uspgr1v1eop  29183  hh0oi  31839  eulerpartlemmf  34373  bnj601  34917  dffv5  35919  zrdivrng  37954  isdrngo1  37957  aks5lem3a  42184  aks5lem7  42195  prjspval2  42608  mapfzcons  42711  mapfzcons1  42712  mapfzcons2  42714  df3o3  43310  fourierdlem80  46191  lmod1zr  48486  ovsng2  48851  setc1oterm  49484  setc1ohomfval  49486  setc1ocofval  49487  funcsetc1o  49490  termcfuncval  49525  termcnatval  49528