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

Theorem breq12 4028
Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
Assertion
Ref Expression
breq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breq12
StepHypRef Expression
1 breq1 4026 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4027 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 680 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  breq12i  4032  breq12d  4036  breqan12d  4038  posn  4758  isopolem  5842  poxp  6227  soxp  6228  fnse  6232  ecopover  6762  canth2g  7015  infxpen  7642  sornom  7903  dcomex  8073  zorn2lem6  8128  brdom6disj  8157  fpwwe2  8265  rankcf  8399  ltresr  8762  ltxrlt  8893  wloglei  9305  ltxr  10457  xrltnr  10462  xrltnsym  10471  xrlttri  10473  xrlttr  10474  f1olecpbl  13429  isfull  13784  isfth  13788  prslem  14065  pslem  14315  dirtr  14358  xrsdsval  16415  dvcvx  19367  dfrel4  23204  iseupa  23881  dfpo2  24112  fununiq  24126  elfix2  24444  axcontlem9  24600  preoref22  25229  monotoddzzfi  27027  iscusgra  28153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator