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

Theorem breq12 4220
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 4218 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4219 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 682 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   class class class wbr 4215
This theorem is referenced by:  breq12i  4224  breq12d  4228  breqan12d  4230  posn  4949  isopolem  6068  poxp  6461  soxp  6462  fnse  6466  isprmpt2  6480  ecopover  7011  canth2g  7264  infxpen  7901  sornom  8162  dcomex  8332  zorn2lem6  8386  brdom6disj  8415  fpwwe2  8523  rankcf  8657  ltresr  9020  ltxrlt  9151  wloglei  9564  ltxr  10720  xrltnr  10725  xrltnsym  10735  xrlttri  10737  xrlttr  10738  brfi1uzind  11720  f1olecpbl  13757  isfull  14112  isfth  14116  prslem  14393  pslem  14643  dirtr  14686  xrsdsval  16747  dvcvx  19909  iscusgra  21470  sizeusglecusg  21500  iswlkon  21536  istrlon  21546  ispth  21573  isspth  21574  ispthon  21581  0pthonv  21586  isspthon  21588  1pthon2v  21598  2pthon3v  21609  constr3cyclpe  21655  3v3e3cycl2  21656  iseupa  21692  dfrel4  24039  dfpo2  25383  fununiq  25399  elfix2  25754  axcontlem9  25916  monotoddzzfi  27019  usg2wlk  28357  usg2wlkon  28358  isrusgra  28442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216
  Copyright terms: Public domain W3C validator