Theorem sneqi 4602

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

This proof depends on syntax axioms:   = wceq 1570  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-sn 4592

This theorem is used by:  fnressn  7161  fressnfv  7163  snriota  7409  xpassen  9066  ids1  14656  s3tpop  14972  bpoly3  16136  strle1  17242  2strop  17313  ghmeqker  19359  pws1  20454  pwsmgp  20456  lpival  21544  mat1dimelbas  22680  mat1dim0  22682  mat1dimid  22683  mat1dimscm  22684  mat1dimmul  22685  mat1f1o  22687  imasdsf1olem  24583  ehl0  25629  nosupcbv  27919  noinfcbv  27934  bday1  28060  bdaypw2n0bndlem  28709  vtxval3sn  29450  iedgval3sn  29451  uspgr1v1eop  29659  hh0oi  32328  selvply1rhm0  33982  eulerpartlemmf  34832  bnj601  35375  dffv5  36453  zrdivrng  38664  isdrngo1  38667  aks5lem3a  43016  aks5lem7  43027  prjspval2  43405  mapfzcons  43507  mapfzcons1  43508  mapfzcons2  43510  df3o3  44101  fourierdlem80  46960  isprmrng  49160  lmod1zr  49332  ovsng2  49696  setc1oterm  50328  setc1ohomfval  50330  setc1ocofval  50331  funcsetc1o  50334  termcfuncval  50369  termcnatval  50372