Theorem sneqi 4600

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

Syntax hints:   = wceq 1570  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-sn 4590

This theorem is referenced by:  fnressn  7155  fressnfv  7157  snriota  7400  xpassen  9055  ids1  14631  s3tpop  14942  bpoly3  16107  strle1  17213  2strop  17284  ghmeqker  19308  pws1  20402  pwsmgp  20404  lpival  21492  mat1dimelbas  22628  mat1dim0  22630  mat1dimid  22631  mat1dimscm  22632  mat1dimmul  22633  mat1f1o  22635  imasdsf1olem  24530  ehl0  25576  nosupcbv  27866  noinfcbv  27881  bday1  28007  bdaypw2n0bndlem  28656  vtxval3sn  29393  iedgval3sn  29394  uspgr1v1eop  29599  hh0oi  32255  selvply1rhm0  33916  eulerpartlemmf  34765  bnj601  35308  dffv5  36414  zrdivrng  38624  isdrngo1  38627  aks5lem3a  42976  aks5lem7  42987  prjspval2  43365  mapfzcons  43467  mapfzcons1  43468  mapfzcons2  43470  df3o3  44061  fourierdlem80  46920  isprmrng  49121  lmod1zr  49293  ovsng2  49657  setc1oterm  50289  setc1ohomfval  50291  setc1ocofval  50292  funcsetc1o  50295  termcfuncval  50330  termcnatval  50333