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

Theorem breq 4291
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 2502 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4290 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4290 . 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 1364    e. wcel 1761   <.cop 3880   class class class wbr 4289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2434  df-clel 2437  df-br 4290
This theorem is referenced by:  breqi  4295  breqd  4300  poeq1  4640  soeq1  4656  freq1  4686  fveq1  5687  foeqcnvco  5995  f1eqcocnv  5996  isoeq2  6008  isoeq3  6009  ofreq  6322  supeq3  7695  oieq1  7722  dcomex  8612  axdc2lem  8613  brdom3  8691  brdom7disj  8694  brdom6disj  8695  shftfval  12555  isprs  15096  isdrs  15100  ispos  15113  istos  15201  efglem  16206  frgpuplem  16262  ordtval  18752  utop2nei  19784  utop3cls  19785  isucn2  19813  ucnima  19815  iducn  19817  ex-opab  23574  resspos  26053  relexpindlem  27270  dfrtrclrec2  27274  rtrclreclem.trans  27277  rtrclind  27280  brabsb2  28932
  Copyright terms: Public domain W3C validator