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

Theorem breqi 4210
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 4206 . 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 1652   class class class wbr 4204
This theorem is referenced by:  brabsbOLD  4456  f1ompt  5883  isocnv3  6044  brtpos2  6477  brwitnlem  6743  brdifun  6924  omxpenlem  7201  infxpenlem  7887  ltpiord  8756  nqerf  8799  nqerid  8802  ordpinq  8812  ltxrlt  9138  ltxr  10707  oduleg  14551  oduposb  14555  xmeterval  18454  pi1cpbl  19061  avril1  21749  axhcompl-zf  22493  hlimadd  22687  hhcmpl  22694  hhcms  22697  hlim0  22730  isarchi  24244  pstmfval  24283  pstmxmet  24284  lmlim  24325  brtxp  25717  brpprod  25722  brpprod3b  25724  brtxpsd2  25732  brdomain  25770  brrange  25771  brimg  25774  brapply  25775  brsuccf  25778  brrestrict  25786  brub  25791  brlb  25792  brbtwn  25830  colineardim1  25987  broutsideof  26047  fneval  26358  climreeq  27706  gte-lte  28404  gt-lt  28405  gte-lteh  28406  gt-lth  28407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431  df-br 4205
  Copyright terms: Public domain W3C validator