Theorem sneqi 4577

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

Syntax hints:   = wceq 1541  {csn 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-sn 4567

This theorem is referenced by:  fnressn  7024  fressnfv  7026  snriota  7259  xpassen  8822  ids1  14283  s3tpop  14603  bpoly3  15749  strle1  16840  2strop1  16921  ghmeqker  18842  pws1  19836  pwsmgp  19838  lpival  20497  mat1dimelbas  21601  mat1dim0  21603  mat1dimid  21604  mat1dimscm  21605  mat1dimmul  21606  mat1f1o  21608  imasdsf1olem  23507  ehl0  24562  vtxval3sn  27394  iedgval3sn  27395  uspgr1v1eop  27597  hh0oi  30244  eulerpartlemmf  32321  bnj601  32879  nosupcbv  33884  noinfcbv  33899  bday1s  34004  dffv5  34205  zrdivrng  36090  isdrngo1  36093  prjspval2  40432  mapfzcons  40518  mapfzcons1  40519  mapfzcons2  40521  df3o3  41588  fourierdlem80  43681  lmod1zr  45786  mndtchom  46323