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

Theorem breq12 4044
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 4042 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4043 . 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 1632   class class class wbr 4039
This theorem is referenced by:  breq12i  4048  breq12d  4052  breqan12d  4054  posn  4774  isopolem  5858  poxp  6243  soxp  6244  fnse  6248  ecopover  6778  canth2g  7031  infxpen  7658  sornom  7919  dcomex  8089  zorn2lem6  8144  brdom6disj  8173  fpwwe2  8281  rankcf  8415  ltresr  8778  ltxrlt  8909  wloglei  9321  ltxr  10473  xrltnr  10478  xrltnsym  10487  xrlttri  10489  xrlttr  10490  f1olecpbl  13445  isfull  13800  isfth  13804  prslem  14081  pslem  14331  dirtr  14374  xrsdsval  16431  dvcvx  19383  dfrel4  23219  iseupa  23896  dfpo2  24183  fununiq  24197  elfix2  24515  axcontlem9  24672  preoref22  25332  monotoddzzfi  27130  isprmpt2  28208  iscusgra  28292  iswlkon  28332  istrlon  28340  ispth  28354  isspth  28355  ispthon  28362  constr3cyclpe  28409  3v3e3cycl2  28410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator