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

Theorem breqi 4398
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 4394 . 2  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
31, 2ax-mp 5 1  |-  ( A R B  <->  A S B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370   class class class wbr 4392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446  df-br 4393
This theorem is referenced by:  f1ompt  5966  isocnv3  6124  brtpos2  6853  brwitnlem  7049  brdifun  7230  omxpenlem  7514  infxpenlem  8283  ltpiord  9159  nqerf  9202  nqerid  9205  ordpinq  9215  ltxrlt  9548  ltxr  11198  oduleg  15406  oduposb  15410  meet0  15411  join0  15412  xmeterval  20125  pi1cpbl  20734  brbtwn  23282  avril1  23793  axhcompl-zf  24537  hlimadd  24732  hhcmpl  24739  hhcms  24742  hlim0  24775  posrasymb  26254  trleile  26263  isarchi  26335  pstmfval  26459  pstmxmet  26460  lmlim  26513  brtxp  28047  brpprod  28052  brpprod3b  28054  brtxpsd2  28062  brdomain  28100  brrange  28101  brimg  28104  brapply  28105  brsuccf  28108  brrestrict  28116  brub  28121  brlb  28122  colineardim1  28228  broutsideof  28288  fneval  28699  climreeq  29926  rgraprop  30685  rusgraprop  30686  rusgrargra  30687  gte-lte  31357  gt-lt  31358  gte-lteh  31359  gt-lth  31360
  Copyright terms: Public domain W3C validator