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

Theorem sneqi 4601
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 4600 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  {csn 4590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-sn 4591
This theorem is referenced by:  fnressn  7108  fressnfv  7110  snriota  7351  xpassen  9016  ids1  14494  s3tpop  14807  bpoly3  15949  strle1  17038  2strop1  17119  ghmeqker  19043  pws1  20048  pwsmgp  20050  lpival  20760  mat1dimelbas  21843  mat1dim0  21845  mat1dimid  21846  mat1dimscm  21847  mat1dimmul  21848  mat1f1o  21850  imasdsf1olem  23749  ehl0  24804  nosupcbv  27073  noinfcbv  27088  bday1s  27199  vtxval3sn  28043  iedgval3sn  28044  uspgr1v1eop  28246  hh0oi  30894  eulerpartlemmf  33039  bnj601  33596  dffv5  34562  zrdivrng  36462  isdrngo1  36465  prjspval2  40998  mapfzcons  41086  mapfzcons1  41087  mapfzcons2  41089  df3o3  41696  fourierdlem80  44517  lmod1zr  46664  mndtchom  47200
  Copyright terms: Public domain W3C validator