Theorem breqtrri 5146

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 2744	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtri 5144	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1540   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  3brtr4i  5149  ensn1  9035  1sdom2ALT  9249  dju1p1e2ALT  10189  infmap2  10231  0lt1sr  11109  0le2  12342  2pos  12343  3pos  12345  4pos  12347  5pos  12349  6pos  12350  7pos  12351  8pos  12352  9pos  12353  1lt2  12411  2lt3  12412  3lt4  12414  4lt5  12417  5lt6  12421  6lt7  12426  7lt8  12432  8lt9  12439  numltc  12734  declti  12746  xlemul1a  13304  sqge0i  14206  faclbnd2  14309  cats1fv  14878  ege2le3  16106  cos2bnd  16206  3dvdsdec  16351  n2dvdsm1  16388  sumeven  16406  divalglem2  16414  pockthi  16927  dec2dvds  17083  prmlem1  17127  prmlem2  17139  1259prm  17155  2503prm  17159  4001prm  17164  vitalilem5  25565  dveflem  25935  tangtx  26466  sinq12ge0  26469  logi  26548  cxpge0  26644  asin1  26856  birthday  26916  lgamgulmlem4  26994  ppiub  27167  bposlem7  27253  lgsdir2lem2  27289  pthdlem2  29750  ex-fl  30428  ex-ind-dvds  30442  siilem2  30833  normlem6  31096  normlem7  31097  cm2mi  31607  pjnormi  31702  unierri  32085  dp2lt10  32858  dpgti  32880  pfx1s2  32914  cyc2fv2  33133  cyc3fv3  33150  hgt750lemd  34680  hgt750lem  34683  hgt750lem2  34684  hgt750leme  34690  cnndvlem1  36555  taupi  37341  poimirlem25  37669  poimirlem26  37670  poimirlem27  37671  poimirlem28  37672  ftc1anclem5  37721  fdc  37769  lcmineqlem23  42064  3lexlogpow2ineq2  42072  pellfundgt1  42906  jm2.27dlem2  43034  stoweidlem13  46042  sqwvfoura  46257  sqwvfourb  46258  fourierswlem  46259  tworepnotupword  46915  m1modnep2mod  47381  41prothprm  47633  tgblthelfgott  47829  tgoldbachlt  47830  nnlog2ge0lt1  48546  1aryenefmnd  48626  ackval42  48676