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

Theorem breq12 4442
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 4440 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
2 breq2 4441 . 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 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  breq12i  4446  breq12d  4450  breqan12d  4452  posn  5058  isopolem  6226  poxp  6897  soxp  6898  fnse  6902  isprmpt2  6955  ecopover  7417  canth2g  7673  infxpen  8395  sornom  8660  dcomex  8830  zorn2lem6  8884  brdom6disj  8913  fpwwe2  9024  rankcf  9158  ltresr  9520  ltxrlt  9658  wloglei  10092  ltxr  11335  xrltnr  11341  xrltnsym  11354  xrlttri  11356  xrlttr  11357  brfi1uzind  12514  f1olecpbl  14906  isfull  15258  isfth  15262  prslem  15539  pslem  15815  dirtr  15845  xrsdsval  18441  dvcvx  22399  axcontlem9  24253  iscusgra  24434  sizeusglecusg  24464  iswlkon  24512  istrlon  24521  ispth  24548  isspth  24549  ispthon  24556  0pthonv  24561  isspthon  24563  1pthon2v  24573  2pthon3v  24584  usg2wlk  24595  usg2wlkon  24596  constr3cyclpe  24641  3v3e3cycl2  24642  isclwlk0  24732  isrusgra  24905  iseupa  24943  dfrel4  27432  2sqmo  27615  mclsppslem  28921  dfpo2  29160  fununiq  29176  elfix2  29530  monotoddzzfi  30854  wlkc  32304  lindepsnlininds  32923
  Copyright terms: Public domain W3C validator