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

Theorem breq 4439
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 2516 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4438 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4438 . 2  |-  ( A S B  <->  <. A ,  B >.  e.  S )
41, 2, 33bitr4g 288 1  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   <.cop 4020   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438  df-br 4438
This theorem is referenced by:  breqi  4443  breqd  4448  poeq1  4793  soeq1  4809  freq1  4839  fveq1  5855  foeqcnvco  6188  f1eqcocnv  6189  isoeq2  6201  isoeq3  6202  ofreq  6528  supeq3  7911  oieq1  7940  dcomex  8830  axdc2lem  8831  brdom3  8909  brdom7disj  8912  brdom6disj  8913  shftfval  12885  isprs  15538  isdrs  15542  ispos  15555  istos  15644  efglem  16713  frgpuplem  16769  ordtval  19668  utop2nei  20731  utop3cls  20732  isucn2  20760  ucnima  20762  iducn  20764  ex-opab  25131  resspos  27625  relexpindlem  29040  dfrtrclrec2  29044  rtrclreclem.trans  29047  rtrclind  29050  brabsb2  30579
  Copyright terms: Public domain W3C validator