Theorem sneqi 4591

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

Syntax hints:   = wceq 1541  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-sn 4581

This theorem is referenced by:  fnressn  7103  fressnfv  7105  snriota  7348  xpassen  8999  ids1  14521  s3tpop  14832  bpoly3  15981  strle1  17085  2strop  17156  ghmeqker  19172  pws1  20260  pwsmgp  20262  lpival  21279  mat1dimelbas  22415  mat1dim0  22417  mat1dimid  22418  mat1dimscm  22419  mat1dimmul  22420  mat1f1o  22422  imasdsf1olem  24317  ehl0  25373  nosupcbv  27670  noinfcbv  27685  bday1  27810  bdaypw2n0bndlem  28459  vtxval3sn  29116  iedgval3sn  29117  uspgr1v1eop  29322  hh0oi  31978  eulerpartlemmf  34532  bnj601  35076  dffv5  36116  zrdivrng  38154  isdrngo1  38157  aks5lem3a  42453  aks5lem7  42464  prjspval2  42866  mapfzcons  42968  mapfzcons1  42969  mapfzcons2  42971  df3o3  43566  fourierdlem80  46440  lmod1zr  48749  ovsng2  49114  setc1oterm  49746  setc1ohomfval  49748  setc1ocofval  49749  funcsetc1o  49752  termcfuncval  49787  termcnatval  49790