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

Theorem breqi 4045
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 4041 . 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 1632   class class class wbr 4039
This theorem is referenced by:  brabsbOLD  4290  f1ompt  5698  isocnv3  5845  brtpos2  6256  brwitnlem  6522  brdifun  6703  omxpenlem  6979  infxpenlem  7657  ltpiord  8527  nqerf  8570  nqerid  8573  ordpinq  8583  ltxrlt  8909  ltxr  10473  oduleg  14252  oduposb  14256  xmeterval  17994  pi1cpbl  18558  avril1  20852  axhcompl-zf  21594  hlimadd  21788  hhcmpl  21795  hhcms  21798  hlim0  21831  lmlim  23386  brtxp  24491  brpprod  24496  brpprod3b  24498  brtxpsd2  24506  brdomain  24543  brrange  24544  brimg  24547  brapply  24548  brsuccf  24551  brrestrict  24559  brbtwn  24599  colineardim1  24756  broutsideof  24816  isoriso  25315  fneval  26390  climreeq  27842  gte-lte  28448  gt-lt  28449  gte-lteh  28450  gt-lth  28451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292  df-br 4040
  Copyright terms: Public domain W3C validator