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

Theorem breq 4369
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 2455 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4368 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4368 . 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 1399    e. wcel 1826   <.cop 3950   class class class wbr 4367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-cleq 2374  df-clel 2377  df-br 4368
This theorem is referenced by:  breqi  4373  breqd  4378  poeq1  4717  soeq1  4733  freq1  4763  fveq1  5773  foeqcnvco  6104  f1eqcocnv  6105  isoeq2  6117  isoeq3  6118  ofreq  6442  supeq3  7823  oieq1  7852  dcomex  8740  axdc2lem  8741  brdom3  8819  brdom7disj  8822  brdom6disj  8823  dfrtrclrec2  12892  rtrclreclem3  12895  relexpindlem  12898  rtrclind  12900  shftfval  12905  isprs  15676  isdrs  15680  ispos  15693  istos  15782  efglem  16851  frgpuplem  16907  ordtval  19776  utop2nei  20838  utop3cls  20839  isucn2  20867  ucnima  20869  iducn  20871  ex-opab  25274  resspos  27800  brabsb2  30769
  Copyright terms: Public domain W3C validator