Theorem sneqi 4593

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

Syntax hints:   = wceq 1542  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4583

This theorem is referenced by:  fnressn  7113  fressnfv  7115  snriota  7358  xpassen  9011  ids1  14533  s3tpop  14844  bpoly3  15993  strle1  17097  2strop  17168  ghmeqker  19184  pws1  20272  pwsmgp  20274  lpival  21291  mat1dimelbas  22427  mat1dim0  22429  mat1dimid  22430  mat1dimscm  22431  mat1dimmul  22432  mat1f1o  22434  imasdsf1olem  24329  ehl0  25385  nosupcbv  27682  noinfcbv  27697  bday1  27822  bdaypw2n0bndlem  28471  vtxval3sn  29128  iedgval3sn  29129  uspgr1v1eop  29334  hh0oi  31991  eulerpartlemmf  34553  bnj601  35096  dffv5  36138  zrdivrng  38204  isdrngo1  38207  aks5lem3a  42559  aks5lem7  42570  prjspval2  42971  mapfzcons  43073  mapfzcons1  43074  mapfzcons2  43076  df3o3  43671  fourierdlem80  46544  lmod1zr  48853  ovsng2  49218  setc1oterm  49850  setc1ohomfval  49852  setc1ocofval  49853  funcsetc1o  49856  termcfuncval  49891  termcnatval  49894