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

Theorem breqtrri 4422
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
breqtrr.1  |-  A R B
breqtrr.2  |-  C  =  B
Assertion
Ref Expression
breqtrri  |-  A R C

Proof of Theorem breqtrri
StepHypRef Expression
1 breqtrr.1 . 2  |-  A R B
2 breqtrr.2 . . 3  |-  C  =  B
32eqcomi 2417 . 2  |-  B  =  C
41, 3breqtri 4420 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1407   class class class wbr 4397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-br 4398
This theorem is referenced by:  3brtr4i  4425  ensn1  7619  1sdom2  7756  pm110.643ALT  8592  infmap2  8632  0lt1sr  9504  0le2  10669  2pos  10670  3pos  10672  4pos  10674  5pos  10676  6pos  10677  7pos  10678  8pos  10679  9pos  10680  10pos  10681  1lt2  10745  2lt3  10746  3lt4  10748  4lt5  10751  5lt6  10755  6lt7  10760  7lt8  10766  8lt9  10773  9lt10  10781  nn0le2xi  10890  numltc  11041  declti  11046  xlemul1a  11535  sqge0i  12302  faclbnd2  12415  cats1fv  12882  ege2le3  14036  cos2bnd  14134  divalglem2  14264  pockthi  14636  dec2dvds  14760  prmlem1  14804  prmlem2  14816  1259prm  14829  2503prm  14833  4001prm  14838  vitalilem5  22315  dveflem  22674  tangtx  23192  sinq12ge0  23195  cxpge0  23360  asin1  23552  birthday  23612  lgamgulmlem4  23689  ppiub  23862  bposlem4  23945  bposlem5  23946  bposlem7  23948  lgsdir2lem2  23982  ex-fl  25598  ex-ind-dvds  25600  siilem2  26194  normlem6  26459  normlem7  26460  cm2mi  26971  pjnormi  27066  unierri  27449  logi  29956  taupi  31262  ftc1anclem5  31480  fdc  31533  pellfundgt1  35193  jm2.27dlem2  35327  stoweidlem13  37176  sqwvfoura  37392  sqwvfourb  37393  fourierswlem  37394  41prothprm  37878  nnlog2ge0lt1  38710
  Copyright terms: Public domain W3C validator