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

Theorem breq 4216
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 2499 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4215 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4215 . 2  |-  ( A S B  <->  <. A ,  B >.  e.  S )
41, 2, 33bitr4g 281 1  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   <.cop 3819   class class class wbr 4214
This theorem is referenced by:  breqi  4220  breqd  4225  poeq1  4508  soeq1  4524  freq1  4554  fveq1  5729  foeqcnvco  6029  f1eqcocnv  6030  isoeq2  6042  isoeq3  6043  ofreq  6310  supeq3  7456  oieq1  7483  dcomex  8329  axdc2lem  8330  brdom3  8408  brdom7disj  8411  brdom6disj  8412  shftfval  11887  isprs  14389  isdrs  14393  ispos  14406  istos  14466  spwval2  14658  efglem  15350  frgpuplem  15406  ordtval  17255  utop2nei  18282  utop3cls  18283  isucn2  18311  ucnima  18313  iducn  18315  ex-opab  21742  resspos  24189  relexpindlem  25141  dfrtrclrec2  25145  rtrclreclem.trans  25148  rtrclind  25151  brabsb2  26713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434  df-br 4215
  Copyright terms: Public domain W3C validator