MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneqi Structured version   Visualization version   GIF version

Theorem sneqi 4551
Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqi.1 𝐴 = 𝐵
Assertion
Ref Expression
sneqi {𝐴} = {𝐵}

Proof of Theorem sneqi
StepHypRef Expression
1 sneqi.1 . 2 𝐴 = 𝐵
2 sneq 4550 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  {csn 4540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-sn 4541
This theorem is referenced by:  fnressn  6893  fressnfv  6895  snriota  7121  xpassen  8586  ids1  13930  s3tpop  14250  bpoly3  15391  strle1  16570  2strop1  16585  ghmeqker  18363  pws1  19344  pwsmgp  19346  lpival  19993  mat1dimelbas  21055  mat1dim0  21057  mat1dimid  21058  mat1dimscm  21059  mat1dimmul  21060  mat1f1o  21062  imasdsf1olem  22958  ehl0  23999  vtxval3sn  26814  iedgval3sn  26815  uspgr1v1eop  27017  hh0oi  29664  eulerpartlemmf  31640  bnj601  32199  dffv5  33392  zrdivrng  35269  isdrngo1  35272  fnimasnd  39235  prjspval2  39402  mapfzcons  39452  mapfzcons1  39453  mapfzcons2  39455  df3o3  40510  fourierdlem80  42619  lmod1zr  44693
  Copyright terms: Public domain W3C validator