Theorem sneqi 4596

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

Syntax hints:   = wceq 1540  {csn 4585

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4586

This theorem is referenced by:  fnressn  7112  fressnfv  7114  snriota  7359  xpassen  9012  ids1  14538  s3tpop  14851  bpoly3  16000  strle1  17104  2strop  17175  ghmeqker  19151  pws1  20210  pwsmgp  20212  lpival  21210  mat1dimelbas  22334  mat1dim0  22336  mat1dimid  22337  mat1dimscm  22338  mat1dimmul  22339  mat1f1o  22341  imasdsf1olem  24237  ehl0  25293  nosupcbv  27590  noinfcbv  27605  bday1s  27719  vtxval3sn  28946  iedgval3sn  28947  uspgr1v1eop  29152  hh0oi  31805  eulerpartlemmf  34339  bnj601  34883  dffv5  35885  zrdivrng  37920  isdrngo1  37923  aks5lem3a  42150  aks5lem7  42161  prjspval2  42574  mapfzcons  42677  mapfzcons1  42678  mapfzcons2  42680  df3o3  43276  fourierdlem80  46157  lmod1zr  48455  ovsng2  48820  setc1oterm  49453  setc1ohomfval  49455  setc1ocofval  49456  funcsetc1o  49459  termcfuncval  49494  termcnatval  49497