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

Theorem sneqi 4221
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 4220 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2ax-mp 5 1 {𝐴} = {𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sn 4211
This theorem is referenced by:  fnressn  6465  fressnfv  6467  snriota  6681  xpassen  8095  ids1  13413  s3tpop  13700  bpoly3  14833  strlemor1OLD  16016  strle1  16020  2strop1  16035  ghmeqker  17734  pws1  18662  pwsmgp  18664  lpival  19293  mat1dimelbas  20325  mat1dim0  20327  mat1dimid  20328  mat1dimscm  20329  mat1dimmul  20330  mat1f1o  20332  imasdsf1olem  22225  vtxval3sn  25980  iedgval3sn  25981  uspgr1v1eop  26186  hh0oi  28890  eulerpartlemmf  30565  bnj601  31116  dffv5  32156  zrdivrng  33882  isdrngo1  33885  mapfzcons  37596  mapfzcons1  37597  mapfzcons2  37599  df3o3  38640  fourierdlem80  40721  lmod1zr  42607
  Copyright terms: Public domain W3C validator