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

Theorem breq 4449
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 2540 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4448 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4448 . 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 1379    e. wcel 1767   <.cop 4033   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462  df-br 4448
This theorem is referenced by:  breqi  4453  breqd  4458  poeq1  4803  soeq1  4819  freq1  4849  fveq1  5863  foeqcnvco  6189  f1eqcocnv  6190  isoeq2  6202  isoeq3  6203  ofreq  6525  supeq3  7905  oieq1  7933  dcomex  8823  axdc2lem  8824  brdom3  8902  brdom7disj  8905  brdom6disj  8906  shftfval  12862  isprs  15413  isdrs  15417  ispos  15430  istos  15518  efglem  16530  frgpuplem  16586  ordtval  19456  utop2nei  20488  utop3cls  20489  isucn2  20517  ucnima  20519  iducn  20521  ex-opab  24830  resspos  27309  relexpindlem  28537  dfrtrclrec2  28541  rtrclreclem.trans  28544  rtrclind  28547  brabsb2  30207
  Copyright terms: Public domain W3C validator