Theorem sneqi 4595

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

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

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-sn 4585

This theorem is used by:  fnressn  7162  fressnfv  7164  snriota  7410  xpassen  9090  ids1  14744  s3tpop  15060  bpoly3  16224  strle1  17336  2strop  17407  ghmeqker  19457  pws1  20554  pwsmgp  20556  lpival  21648  mat1dimelbas  22786  mat1dim0  22788  mat1dimid  22789  mat1dimscm  22790  mat1dimmul  22791  mat1f1o  22793  imasdsf1olem  24692  ehl0  25738  nosupcbv  28059  noinfcbv  28074  bday1  28200  bdaypw2n0bndlem  28849  vtxval3sn  29621  iedgval3sn  29622  uspgr1v1eop  29830  hh0oi  32505  selvply1rhm0  34158  eulerpartlemmf  35007  bnj601  35550  dffv5  36686  zrdivrng  38887  isdrngo1  38890  aks5lem3a  43239  aks5lem7  43250  prjspval2  43641  mapfzcons  43726  mapfzcons1  43727  mapfzcons2  43729  df3o3  44315  fourierdlem80  47195  isprmrng  49432  lmod1zr  49604  ovsng2  49968  setc1oterm  50598  setc1ohomfval  50600  setc1ocofval  50601  funcsetc1o  50604  termcfuncval  50639  termcnatval  50642