Theorem sneqi 4642

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

Syntax hints:   = wceq 1537  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-sn 4632

This theorem is referenced by:  fnressn  7178  fressnfv  7180  snriota  7421  xpassen  9105  ids1  14632  s3tpop  14945  bpoly3  16091  strle1  17192  2strop1  17273  ghmeqker  19274  pws1  20339  pwsmgp  20341  lpival  21352  mat1dimelbas  22493  mat1dim0  22495  mat1dimid  22496  mat1dimscm  22497  mat1dimmul  22498  mat1f1o  22500  imasdsf1olem  24399  ehl0  25465  nosupcbv  27762  noinfcbv  27777  bday1s  27891  cutpw2  28432  pw2bday  28433  vtxval3sn  29075  iedgval3sn  29076  uspgr1v1eop  29281  hh0oi  31932  eulerpartlemmf  34357  bnj601  34913  dffv5  35906  zrdivrng  37940  isdrngo1  37943  aks5lem3a  42171  aks5lem7  42182  prjspval2  42600  mapfzcons  42704  mapfzcons1  42705  mapfzcons2  42707  df3o3  43304  fourierdlem80  46142  lmod1zr  48339  mndtchom  48893