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

Theorem sneqi 3886
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 3885 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2ax-mp 5 1  |-  { A }  =  { B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   {csn 3875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-sn 3876
This theorem is referenced by:  fnressn  5892  fressnfv  5894  snriota  6080  xpassen  7403  ids1  12287  strlemor1  14263  strle1  14267  ghmeqker  15771  pws1  16706  pwsmgp  16708  lpival  17325  imasdsf1olem  19946  vdgr1c  23573  ginvsn  23834  zrdivrng  23917  hh0oi  25305  eulerpartlemmf  26756  dffv5  27953  bpoly3  28199  isdrngo1  28759  mapfzcons  29049  mapfzcons1  29050  mapfzcons2  29052  mat1dimelbas  30864  mat1dim0  30866  mat1dimid  30867  mat1dimscm  30868  mat1dimmul  30869  lmod1zr  31032  bnj601  31910
  Copyright terms: Public domain W3C validator