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

Theorem sneqi 4410
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 4409 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  {csn 4399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-sn 4400
This theorem is referenced by:  fnressn  6681  fressnfv  6683  snriota  6901  xpassen  8329  ids1  13664  s3tpop  14037  bpoly3  15168  strle1  16339  2strop1  16354  ghmeqker  18045  pws1  18977  pwsmgp  18979  lpival  19613  mat1dimelbas  20652  mat1dim0  20654  mat1dimid  20655  mat1dimscm  20656  mat1dimmul  20657  mat1f1o  20659  imasdsf1olem  22555  ehl0  23592  vtxval3sn  26348  iedgval3sn  26349  uspgr1v1eop  26553  hh0oi  29313  eulerpartlemmf  30978  bnj601  31532  dffv5  32565  zrdivrng  34293  isdrngo1  34296  mapfzcons  38122  mapfzcons1  38123  mapfzcons2  38125  df3o3  39162  fourierdlem80  41195  lmod1zr  43147
  Copyright terms: Public domain W3C validator