ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq Unicode version

Theorem breq 3931
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 2203 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 3930 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 3930 . 2  |-  ( A S B  <->  <. A ,  B >.  e.  S )
41, 2, 33bitr4g 222 1  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1331    e. wcel 1480   <.cop 3530   class class class wbr 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-br 3930
This theorem is referenced by:  breqi  3935  breqd  3940  poeq1  4221  soeq1  4237  frforeq1  4265  weeq1  4278  fveq1  5420  foeqcnvco  5691  f1eqcocnv  5692  isoeq2  5703  isoeq3  5704  ofreq  5985  supeq3  6877  shftfvalg  10597  shftfval  10600
  Copyright terms: Public domain W3C validator