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

Theorem breqi 4029
Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
Hypothesis
Ref Expression
breqi.1  |-  R  =  S
Assertion
Ref Expression
breqi  |-  ( A R B  <->  A S B )

Proof of Theorem breqi
StepHypRef Expression
1 breqi.1 . 2  |-  R  =  S
2 breq 4025 . 2  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
31, 2ax-mp 8 1  |-  ( A R B  <->  A S B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  brabsbOLD  4274  f1ompt  5682  isocnv3  5829  brtpos2  6240  brwitnlem  6506  brdifun  6687  omxpenlem  6963  infxpenlem  7641  ltpiord  8511  nqerf  8554  nqerid  8557  ordpinq  8567  ltxrlt  8893  ltxr  10457  oduleg  14236  oduposb  14240  xmeterval  17978  pi1cpbl  18542  avril1  20836  axhcompl-zf  21578  hlimadd  21772  hhcmpl  21779  hhcms  21782  hlim0  21815  lmlim  23371  brtxp  24420  brpprod  24425  brpprod3b  24427  brtxpsd2  24435  brdomain  24472  brrange  24473  brimg  24476  brapply  24477  brsuccf  24480  brrestrict  24487  brbtwn  24527  colineardim1  24684  broutsideof  24744  isoriso  25212  fneval  26287  climreeq  27739  gte-lte  28194  gt-lt  28195  gte-lteh  28196  gt-lth  28197
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279  df-br 4024
  Copyright terms: Public domain W3C validator