Theorem breqtrri 5116

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

Syntax hints:   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  3brtr4i  5119  ensn1  8943  1sdom2ALT  9133  dju1p1e2ALT  10066  infmap2  10108  0lt1sr  10986  0le2  12227  2pos  12228  3pos  12230  4pos  12232  5pos  12234  6pos  12235  7pos  12236  8pos  12237  9pos  12238  1lt2  12291  2lt3  12292  3lt4  12294  4lt5  12297  5lt6  12301  6lt7  12306  7lt8  12312  8lt9  12319  numltc  12614  declti  12626  xlemul1a  13187  sqge0i  14095  faclbnd2  14198  cats1fv  14766  ege2le3  15997  cos2bnd  16097  3dvdsdec  16243  n2dvdsm1  16280  sumeven  16298  divalglem2  16306  pockthi  16819  dec2dvds  16975  prmlem1  17019  prmlem2  17031  1259prm  17047  2503prm  17051  4001prm  17056  vitalilem5  25540  dveflem  25910  tangtx  26441  sinq12ge0  26444  logi  26523  cxpge0  26619  asin1  26831  birthday  26891  lgamgulmlem4  26969  ppiub  27142  bposlem7  27228  lgsdir2lem2  27264  pthdlem2  29746  ex-fl  30427  ex-ind-dvds  30441  siilem2  30832  normlem6  31095  normlem7  31096  cm2mi  31606  pjnormi  31701  unierri  32084  dp2lt10  32864  dpgti  32886  pfx1s2  32920  cyc2fv2  33091  cyc3fv3  33108  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  cnndvlem1  36581  taupi  37367  poimirlem25  37684  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  ftc1anclem5  37736  fdc  37784  lcmineqlem23  42143  3lexlogpow2ineq2  42151  pellfundgt1  42975  jm2.27dlem2  43102  stoweidlem13  46110  sqwvfoura  46325  sqwvfourb  46326  fourierswlem  46327  m1modnep2mod  47451  41prothprm  47718  tgblthelfgott  47914  tgoldbachlt  47915  nnlog2ge0lt1  48666  1aryenefmnd  48746  ackval42  48796