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

Theorem sneqi 4136
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 4135 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sn 4126
This theorem is referenced by:  fnressn  6330  fressnfv  6332  snriota  6540  xpassen  7939  ids1  13230  s3tpop  13504  bpoly3  14628  strlemor1  15796  strle1  15800  2strop1  15814  ghmeqker  17510  pws1  18439  pwsmgp  18441  lpival  19066  mat1dimelbas  20096  mat1dim0  20098  mat1dimid  20099  mat1dimscm  20100  mat1dimmul  20101  mat1f1o  20103  imasdsf1olem  21988  vtxval3sn  25718  iedgval3sn  25719  vdgr1c  26432  hh0oi  28146  eulerpartlemmf  29764  bnj601  30244  dffv5  31201  zrdivrng  32922  isdrngo1  32925  mapfzcons  36297  mapfzcons1  36298  mapfzcons2  36300  df3o3  37343  fourierdlem80  39079  uspgr1v1eop  40475  lmod1zr  42076
  Copyright terms: Public domain W3C validator