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

Theorem sneqi 4568
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 4567 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-sn 4558
This theorem is referenced by:  fnressn  6912  fressnfv  6914  snriota  7136  xpassen  8599  ids1  13939  s3tpop  14259  bpoly3  15400  strle1  16580  2strop1  16595  ghmeqker  18323  pws1  19295  pwsmgp  19297  lpival  19946  mat1dimelbas  21008  mat1dim0  21010  mat1dimid  21011  mat1dimscm  21012  mat1dimmul  21013  mat1f1o  21015  imasdsf1olem  22910  ehl0  23947  vtxval3sn  26755  iedgval3sn  26756  uspgr1v1eop  26958  hh0oi  29607  eulerpartlemmf  31532  bnj601  32091  dffv5  33282  zrdivrng  35112  isdrngo1  35115  fnimasnd  38999  prjspval2  39141  mapfzcons  39191  mapfzcons1  39192  mapfzcons2  39194  df3o3  40253  fourierdlem80  42348  lmod1zr  44476
  Copyright terms: Public domain W3C validator