Theorem sneqi 4324

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

Syntax hints:   = wceq 1624  {csn 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-sn 4314

This theorem is referenced by:  fnressn  6580  fressnfv  6582  snriota  6796  xpassen  8211  ids1  13559  s3tpop  13846  bpoly3  14980  strlemor1OLD  16163  strle1  16167  2strop1  16182  ghmeqker  17880  pws1  18808  pwsmgp  18810  lpival  19439  mat1dimelbas  20471  mat1dim0  20473  mat1dimid  20474  mat1dimscm  20475  mat1dimmul  20476  mat1f1o  20478  imasdsf1olem  22371  vtxval3sn  26126  iedgval3sn  26127  uspgr1v1eop  26332  hh0oi  29063  eulerpartlemmf  30738  bnj601  31289  dffv5  32329  zrdivrng  34057  isdrngo1  34060  mapfzcons  37773  mapfzcons1  37774  mapfzcons2  37776  df3o3  38817  fourierdlem80  40898  lmod1zr  42784