Theorem breqtrri 5066

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
breqtrr.1	⊢ 𝐴𝑅𝐵
breqtrr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrri	⊢ 𝐴𝑅𝐶

Proof of Theorem breqtrri

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2745	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtri 5064	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1543   class class class wbr 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040

This theorem is referenced by:  3brtr4i  5069  ensn1  8672  ensn1OLD  8673  1sdom2  8853  dju1p1e2ALT  9753  infmap2  9797  0lt1sr  10674  0le2  11897  2pos  11898  3pos  11900  4pos  11902  5pos  11904  6pos  11905  7pos  11906  8pos  11907  9pos  11908  1lt2  11966  2lt3  11967  3lt4  11969  4lt5  11972  5lt6  11976  6lt7  11981  7lt8  11987  8lt9  11994  nn0le2xi  12109  numltc  12284  declti  12296  xlemul1a  12843  sqge0i  13722  faclbnd2  13822  cats1fv  14389  ege2le3  15614  cos2bnd  15712  3dvdsdec  15856  n2dvdsm1  15893  sumeven  15911  divalglem2  15919  pockthi  16423  dec2dvds  16579  prmlem1  16624  prmlem2  16636  1259prm  16652  2503prm  16656  4001prm  16661  2strstr1  16789  vitalilem5  24463  dveflem  24830  tangtx  25349  sinq12ge0  25352  cxpge0  25525  asin1  25731  birthday  25791  lgamgulmlem4  25868  ppiub  26039  bposlem7  26125  lgsdir2lem2  26161  pthdlem2  27809  ex-fl  28484  ex-ind-dvds  28498  siilem2  28887  normlem6  29150  normlem7  29151  cm2mi  29661  pjnormi  29756  unierri  30139  dp2lt10  30832  dpgti  30854  pfx1s2  30887  cyc2fv2  31062  cyc3fv3  31079  hgt750lemd  32294  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  logi  33369  cnndvlem1  34403  taupi  35177  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  poimirlem28  35491  ftc1anclem5  35540  fdc  35589  lcmineqlem23  39742  3lexlogpow2ineq2  39750  pellfundgt1  40349  jm2.27dlem2  40476  stoweidlem13  43172  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  41prothprm  44687  tgblthelfgott  44883  tgoldbachlt  44884  nnlog2ge0lt1  45528  1aryenefmnd  45608  ackval42  45658