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

Theorem breq 3967
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 2221 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 3966 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 3966 . 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 1335    e. wcel 2128   <.cop 3563   class class class wbr 3965
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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-br 3966
This theorem is referenced by:  breqi  3971  breqd  3976  poeq1  4259  soeq1  4275  frforeq1  4303  weeq1  4316  fveq1  5467  foeqcnvco  5740  f1eqcocnv  5741  isoeq2  5752  isoeq3  5753  ofreq  6035  supeq3  6934  shftfvalg  10718  shftfval  10721  pw1nct  13586
  Copyright terms: Public domain W3C validator