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

Theorem breq 4041
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 2357 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4040 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4040 . 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 1632    e. wcel 1696   <.cop 3656   class class class wbr 4039
This theorem is referenced by:  breqi  4045  breqd  4050  poeq1  4333  soeq1  4349  freq1  4379  fveq1  5540  foeqcnvco  5820  f1eqcocnv  5821  isoeq2  5833  isoeq3  5834  ofreq  6097  oieq1  7243  dcomex  8089  axdc2lem  8090  brdom3  8169  brdom7disj  8172  brdom6disj  8173  shftfval  11581  isprs  14080  isdrs  14084  ispos  14097  istos  14157  spwval2  14349  efglem  15041  frgpuplem  15097  ordtval  16935  ex-opab  20835  relexpindlem  24051  dfrtrclrec2  24055  rtrclreclem.trans  24058  rtrclind  24061  ubos  25359  mxlelt  25367  mnlelt2  25369  isibcg  26294  brabsb2  26833
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