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

Theorem breq 4174
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 2465 . 2  |-  ( R  =  S  ->  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  S ) )
2 df-br 4173 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  R )
3 df-br 4173 . 2  |-  ( A S B  <->  <. A ,  B >.  e.  S )
41, 2, 33bitr4g 280 1  |-  ( R  =  S  ->  ( A R B  <->  A S B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   <.cop 3777   class class class wbr 4172
This theorem is referenced by:  breqi  4178  breqd  4183  poeq1  4466  soeq1  4482  freq1  4512  fveq1  5686  foeqcnvco  5986  f1eqcocnv  5987  isoeq2  5999  isoeq3  6000  ofreq  6267  oieq1  7437  dcomex  8283  axdc2lem  8284  brdom3  8362  brdom7disj  8365  brdom6disj  8366  shftfval  11840  isprs  14342  isdrs  14346  ispos  14359  istos  14419  spwval2  14611  efglem  15303  frgpuplem  15359  ordtval  17207  utop2nei  18233  utop3cls  18234  isucn2  18262  ucnima  18264  iducn  18266  ex-opab  21693  resspos  24140  relexpindlem  25092  dfrtrclrec2  25096  rtrclreclem.trans  25099  rtrclind  25102  brabsb2  26601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400  df-br 4173
  Copyright terms: Public domain W3C validator