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

Theorem sneqi 4596
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 4595 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  {csn 4585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4586
This theorem is referenced by:  fnressn  7112  fressnfv  7114  snriota  7359  xpassen  9012  ids1  14538  s3tpop  14851  bpoly3  16000  strle1  17104  2strop  17175  ghmeqker  19157  pws1  20245  pwsmgp  20247  lpival  21266  mat1dimelbas  22391  mat1dim0  22393  mat1dimid  22394  mat1dimscm  22395  mat1dimmul  22396  mat1f1o  22398  imasdsf1olem  24294  ehl0  25350  nosupcbv  27647  noinfcbv  27662  bday1s  27780  vtxval3sn  29023  iedgval3sn  29024  uspgr1v1eop  29229  hh0oi  31882  eulerpartlemmf  34359  bnj601  34903  dffv5  35905  zrdivrng  37940  isdrngo1  37943  aks5lem3a  42170  aks5lem7  42181  prjspval2  42594  mapfzcons  42697  mapfzcons1  42698  mapfzcons2  42700  df3o3  43296  fourierdlem80  46177  lmod1zr  48475  ovsng2  48840  setc1oterm  49473  setc1ohomfval  49475  setc1ocofval  49476  funcsetc1o  49479  termcfuncval  49514  termcnatval  49517
  Copyright terms: Public domain W3C validator