Theorem sneqi 4581

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

Syntax hints:   = wceq 1536  {csn 4570

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-sn 4571

This theorem is referenced by:  fnressn  6923  fressnfv  6925  snriota  7150  xpassen  8614  ids1  13954  s3tpop  14274  bpoly3  15415  strle1  16595  2strop1  16610  ghmeqker  18388  pws1  19369  pwsmgp  19371  lpival  20021  mat1dimelbas  21083  mat1dim0  21085  mat1dimid  21086  mat1dimscm  21087  mat1dimmul  21088  mat1f1o  21090  imasdsf1olem  22986  ehl0  24023  vtxval3sn  26831  iedgval3sn  26832  uspgr1v1eop  27034  hh0oi  29683  eulerpartlemmf  31637  bnj601  32196  dffv5  33389  zrdivrng  35235  isdrngo1  35238  fnimasnd  39127  prjspval2  39269  mapfzcons  39319  mapfzcons1  39320  mapfzcons2  39322  df3o3  40381  fourierdlem80  42478  lmod1zr  44555