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

Theorem breq 4025
Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
Assertion
Ref Expression
breq  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )

Proof of Theorem breq
StepHypRef Expression
1 eleq2 2344 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4024 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4024 . 2  |-  ( A S B  <->  <. A ,  B >.  e.  S )
41, 2, 33bitr4g 279 1  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   <.cop 3643   class class class wbr 4023
This theorem is referenced by:  breqi  4029  breqd  4034  poeq1  4317  soeq1  4333  freq1  4363  fveq1  5524  foeqcnvco  5804  f1eqcocnv  5805  isoeq2  5817  isoeq3  5818  ofreq  6081  oieq1  7227  dcomex  8073  axdc2lem  8074  brdom3  8153  brdom7disj  8156  brdom6disj  8157  shftfval  11565  isprs  14064  isdrs  14068  ispos  14081  istos  14141  spwval2  14333  efglem  15025  frgpuplem  15081  ordtval  16919  ex-opab  20819  relexpindlem  24036  dfrtrclrec2  24040  rtrclreclem.trans  24043  rtrclind  24046  ubos  25256  mxlelt  25264  mnlelt2  25266  isibcg  26191  brabsb2  26730
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