Theorem sneqi 4569

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

Syntax hints:   = wceq 1539  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-sn 4559

This theorem is referenced by:  fnressn  7012  fressnfv  7014  snriota  7246  xpassen  8806  ids1  14230  s3tpop  14550  bpoly3  15696  strle1  16787  2strop1  16866  ghmeqker  18776  pws1  19770  pwsmgp  19772  lpival  20429  mat1dimelbas  21528  mat1dim0  21530  mat1dimid  21531  mat1dimscm  21532  mat1dimmul  21533  mat1f1o  21535  imasdsf1olem  23434  ehl0  24486  vtxval3sn  27316  iedgval3sn  27317  uspgr1v1eop  27519  hh0oi  30166  eulerpartlemmf  32242  bnj601  32800  nosupcbv  33832  noinfcbv  33847  bday1s  33952  dffv5  34153  zrdivrng  36038  isdrngo1  36041  prjspval2  40373  mapfzcons  40454  mapfzcons1  40455  mapfzcons2  40457  df3o3  41524  fourierdlem80  43617  lmod1zr  45722  mndtchom  46257