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

Theorem breqi 4160
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 4156 . 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 177    = wceq 1649   class class class wbr 4154
This theorem is referenced by:  brabsbOLD  4406  f1ompt  5831  isocnv3  5992  brtpos2  6422  brwitnlem  6688  brdifun  6869  omxpenlem  7146  infxpenlem  7829  ltpiord  8698  nqerf  8741  nqerid  8744  ordpinq  8754  ltxrlt  9080  ltxr  10648  oduleg  14487  oduposb  14491  xmeterval  18353  pi1cpbl  18941  avril1  21606  axhcompl-zf  22350  hlimadd  22544  hhcmpl  22551  hhcms  22554  hlim0  22587  lmlim  24138  brtxp  25445  brpprod  25450  brpprod3b  25452  brtxpsd2  25460  brdomain  25497  brrange  25498  brimg  25501  brapply  25502  brsuccf  25505  brrestrict  25513  brbtwn  25553  colineardim1  25710  broutsideof  25770  fneval  26059  climreeq  27408  gte-lte  27814  gt-lt  27815  gte-lteh  27816  gt-lth  27817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2381  df-clel 2384  df-br 4155
  Copyright terms: Public domain W3C validator