Theorem sneqi 4572

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

Syntax hints:   = wceq 1539  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-sn 4562

This theorem is referenced by:  fnressn  7030  fressnfv  7032  snriota  7266  xpassen  8853  ids1  14302  s3tpop  14622  bpoly3  15768  strle1  16859  2strop1  16940  ghmeqker  18861  pws1  19855  pwsmgp  19857  lpival  20516  mat1dimelbas  21620  mat1dim0  21622  mat1dimid  21623  mat1dimscm  21624  mat1dimmul  21625  mat1f1o  21627  imasdsf1olem  23526  ehl0  24581  vtxval3sn  27413  iedgval3sn  27414  uspgr1v1eop  27616  hh0oi  30265  eulerpartlemmf  32342  bnj601  32900  nosupcbv  33905  noinfcbv  33920  bday1s  34025  dffv5  34226  zrdivrng  36111  isdrngo1  36114  prjspval2  40452  mapfzcons  40538  mapfzcons1  40539  mapfzcons2  40541  df3o3  41635  fourierdlem80  43727  lmod1zr  45834  mndtchom  46371