Theorem sneqi 4594

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

This proof depends on syntax axioms:   = wceq 1569  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-sn 4588

This theorem is used by:  fnressn  7170  fressnfv  7172  snriota  7417  xpassen  9101  ids1  14754  s3tpop  15072  bpoly3  16236  strle1  17348  2strop  17419  ghmeqker  19469  pws1  20566  pwsmgp  20568  lpival  21660  mat1dimelbas  22798  mat1dim0  22800  mat1dimid  22801  mat1dimscm  22802  mat1dimmul  22803  mat1f1o  22805  imasdsf1olem  24704  ehl0  25750  nosupcbv  28071  noinfcbv  28086  bday1  28212  bdaypw2n0bndlem  28861  vtxval3sn  29633  iedgval3sn  29634  uspgr1v1eop  29842  hh0oi  32517  selvply1rhm0  34211  eulerpartlemmf  35060  bnj601  35603  dffv5  36813  zrdivrng  39027  isdrngo1  39030  aks5lem3a  43379  aks5lem7  43390  prjspval2  43781  mapfzcons  43867  mapfzcons1  43868  mapfzcons2  43870  df3o3  44456  k0004val0  45294  fourierdlem80  47335  isprmrng  49572  lmod1zr  49744  ovsng2  50109  setc1oterm  50765  setc1ohomfval  50767  setc1ocofval  50768  funcsetc1o  50771  termcfuncval  50806  termcnatval  50812