Theorem sneqi 4589

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

Syntax hints:   = wceq 1541  {csn 4578

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-sn 4579

This theorem is referenced by:  fnressn  7101  fressnfv  7103  snriota  7346  xpassen  8997  ids1  14519  s3tpop  14830  bpoly3  15979  strle1  17083  2strop  17154  ghmeqker  19170  pws1  20258  pwsmgp  20260  lpival  21277  mat1dimelbas  22413  mat1dim0  22415  mat1dimid  22416  mat1dimscm  22417  mat1dimmul  22418  mat1f1o  22420  imasdsf1olem  24315  ehl0  25371  nosupcbv  27668  noinfcbv  27683  bday1s  27802  bdaypw2n0s  28420  vtxval3sn  29065  iedgval3sn  29066  uspgr1v1eop  29271  hh0oi  31927  eulerpartlemmf  34481  bnj601  35025  dffv5  36065  zrdivrng  38093  isdrngo1  38096  aks5lem3a  42382  aks5lem7  42393  prjspval2  42798  mapfzcons  42900  mapfzcons1  42901  mapfzcons2  42903  df3o3  43498  fourierdlem80  46372  lmod1zr  48681  ovsng2  49046  setc1oterm  49678  setc1ohomfval  49680  setc1ocofval  49681  funcsetc1o  49684  termcfuncval  49719  termcnatval  49722