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

Theorem breq12 4452
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 4450 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4451 . 2  |-  ( C  =  D  ->  ( B R C  <->  B R D ) )
31, 2sylan9bb 699 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  breq12i  4456  breq12d  4460  breqan12d  4462  posn  5068  isopolem  6229  poxp  6895  soxp  6896  fnse  6900  isprmpt2  6953  ecopover  7415  canth2g  7671  infxpen  8392  sornom  8657  dcomex  8827  zorn2lem6  8881  brdom6disj  8910  fpwwe2  9021  rankcf  9155  ltresr  9517  ltxrlt  9655  wloglei  10085  ltxr  11324  xrltnr  11330  xrltnsym  11343  xrlttri  11345  xrlttr  11346  brfi1uzind  12498  f1olecpbl  14782  isfull  15137  isfth  15141  prslem  15418  pslem  15693  dirtr  15723  xrsdsval  18258  dvcvx  22184  axcontlem9  23979  iscusgra  24160  sizeusglecusg  24190  iswlkon  24238  istrlon  24247  ispth  24274  isspth  24275  ispthon  24282  0pthonv  24287  isspthon  24289  1pthon2v  24299  2pthon3v  24310  usg2wlk  24321  usg2wlkon  24322  constr3cyclpe  24367  3v3e3cycl2  24368  isclwlk0  24458  isrusgra  24631  iseupa  24669  dfrel4  27155  dfpo2  28789  fununiq  28805  elfix2  29159  monotoddzzfi  30510  wlkc  31845  lindepsnlininds  32152
  Copyright terms: Public domain W3C validator