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 2732

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

This theorem is used by:  fnressn  7156  fressnfv  7158  snriota  7404  xpassen  9070  ids1  14665  s3tpop  14981  bpoly3  16145  strle1  17251  2strop  17322  ghmeqker  19371  pws1  20466  pwsmgp  20468  lpival  21556  mat1dimelbas  22694  mat1dim0  22696  mat1dimid  22697  mat1dimscm  22698  mat1dimmul  22699  mat1f1o  22701  imasdsf1olem  24600  ehl0  25646  nosupcbv  27939  noinfcbv  27954  bday1  28080  bdaypw2n0bndlem  28729  vtxval3sn  29501  iedgval3sn  29502  uspgr1v1eop  29710  hh0oi  32385  selvply1rhm0  34037  eulerpartlemmf  34887  bnj601  35430  dffv5  36502  zrdivrng  38704  isdrngo1  38707  aks5lem3a  43056  aks5lem7  43067  prjspval2  43460  mapfzcons  43562  mapfzcons1  43563  mapfzcons2  43565  df3o3  44156  fourierdlem80  47015  isprmrng  49252  lmod1zr  49424  ovsng2  49788  setc1oterm  50418  setc1ohomfval  50420  setc1ocofval  50421  funcsetc1o  50424  termcfuncval  50459  termcnatval  50462