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

Theorem sneqi 4135
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 4134 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-sn 4125
This theorem is referenced by:  fnressn  6308  fressnfv  6310  snriota  6518  xpassen  7916  ids1  13176  s3tpop  13450  bpoly3  14574  strlemor1  15742  strle1  15746  2strop1  15760  ghmeqker  17456  pws1  18385  pwsmgp  18387  lpival  19012  mat1dimelbas  20038  mat1dim0  20040  mat1dimid  20041  mat1dimscm  20042  mat1dimmul  20043  mat1f1o  20045  imasdsf1olem  21929  vdgr1c  26198  hh0oi  27952  eulerpartlemmf  29570  bnj601  30050  dffv5  31007  zrdivrng  32718  isdrngo1  32721  mapfzcons  36093  mapfzcons1  36094  mapfzcons2  36096  df3o3  37139  fourierdlem80  38876  vtxval3sn  40269  iedgval3sn  40270  uspgr1v1eop  40470  lmod1zr  42071
  Copyright terms: Public domain W3C validator