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

Theorem breq 4309
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 2504 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4308 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4308 . 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 1369    e. wcel 1756   <.cop 3898   class class class wbr 4307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439  df-br 4308
This theorem is referenced by:  breqi  4313  breqd  4318  poeq1  4659  soeq1  4675  freq1  4705  fveq1  5705  foeqcnvco  6013  f1eqcocnv  6014  isoeq2  6026  isoeq3  6027  ofreq  6338  supeq3  7714  oieq1  7741  dcomex  8631  axdc2lem  8632  brdom3  8710  brdom7disj  8713  brdom6disj  8714  shftfval  12574  isprs  15115  isdrs  15119  ispos  15132  istos  15220  efglem  16228  frgpuplem  16284  ordtval  18808  utop2nei  19840  utop3cls  19841  isucn2  19869  ucnima  19871  iducn  19873  ex-opab  23654  resspos  26135  relexpindlem  27356  dfrtrclrec2  27360  rtrclreclem.trans  27363  rtrclind  27366  brabsb2  29026
  Copyright terms: Public domain W3C validator