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

Theorem sneqi 3652
Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqi.1  |-  A  =  B
Assertion
Ref Expression
sneqi  |-  { A }  =  { B }

Proof of Theorem sneqi
StepHypRef Expression
1 sneqi.1 . 2  |-  A  =  B
2 sneq 3651 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2ax-mp 8 1  |-  { A }  =  { B }
Colors of variables: wff set class
Syntax hints:    = wceq 1623   {csn 3640
This theorem is referenced by:  fnressn  5705  fressnfv  5707  xpassen  6956  ids1  11437  strlemor1  13235  strle1  13239  ghmeqker  14709  pws1  15399  pwsmgp  15401  lpival  15997  imasdsf1olem  17937  ginvsn  21016  zrdivrng  21099  hh0oi  22483  vdgr1c  23896  dffv5  24463  bpoly3  24793  isdrngo1  26587  mapfzcons  26793  mapfzcons1  26794  mapfzcons2  26796  bnj601  28952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-sn 3646
  Copyright terms: Public domain W3C validator