Theorem sneqi 4641

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

Syntax hints:   = wceq 1533  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-sn 4631

This theorem is referenced by:  fnressn  7167  fressnfv  7169  snriota  7409  xpassen  9091  ids1  14583  s3tpop  14896  bpoly3  16038  strle1  17130  2strop1  17211  ghmeqker  19206  pws1  20273  pwsmgp  20275  lpival  21231  mat1dimelbas  22417  mat1dim0  22419  mat1dimid  22420  mat1dimscm  22421  mat1dimmul  22422  mat1f1o  22424  imasdsf1olem  24323  ehl0  25389  nosupcbv  27681  noinfcbv  27696  bday1s  27810  vtxval3sn  28928  iedgval3sn  28929  uspgr1v1eop  29134  hh0oi  31785  eulerpartlemmf  34126  bnj601  34682  dffv5  35651  zrdivrng  37557  isdrngo1  37560  prjspval2  42172  mapfzcons  42278  mapfzcons1  42279  mapfzcons2  42281  df3o3  42885  fourierdlem80  45712  lmod1zr  47747  mndtchom  48282