Theorem breqtrri 5124

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 5122	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  3brtr4i  5127  ensn1  8960  1sdom2ALT  9151  dju1p1e2ALT  10087  infmap2  10129  0lt1sr  11008  0le2  12249  2pos  12250  3pos  12252  4pos  12254  5pos  12256  6pos  12257  7pos  12258  8pos  12259  9pos  12260  1lt2  12313  2lt3  12314  3lt4  12316  4lt5  12319  5lt6  12323  6lt7  12328  7lt8  12334  8lt9  12341  numltc  12635  declti  12647  xlemul1a  13205  sqge0i  14113  faclbnd2  14216  cats1fv  14784  ege2le3  16015  cos2bnd  16115  3dvdsdec  16261  n2dvdsm1  16298  sumeven  16316  divalglem2  16324  pockthi  16837  dec2dvds  16993  prmlem1  17037  prmlem2  17049  1259prm  17065  2503prm  17069  4001prm  17074  vitalilem5  25571  dveflem  25941  tangtx  26472  sinq12ge0  26475  logi  26554  cxpge0  26650  asin1  26862  birthday  26922  lgamgulmlem4  27000  ppiub  27173  bposlem7  27259  lgsdir2lem2  27295  pthdlem2  29822  ex-fl  30503  ex-ind-dvds  30517  siilem2  30908  normlem6  31171  normlem7  31172  cm2mi  31682  pjnormi  31777  unierri  32160  dp2lt10  32944  dpgti  32966  pfx1s2  33000  cyc2fv2  33183  cyc3fv3  33200  hgt750lemd  34784  hgt750lem  34787  hgt750lem2  34788  hgt750leme  34794  cnndvlem1  36710  taupi  37497  poimirlem25  37815  poimirlem26  37816  poimirlem27  37817  poimirlem28  37818  ftc1anclem5  37867  fdc  37915  lcmineqlem23  42340  3lexlogpow2ineq2  42348  pellfundgt1  43162  jm2.27dlem2  43289  stoweidlem13  46294  sqwvfoura  46509  sqwvfourb  46510  fourierswlem  46511  m1modnep2mod  47635  41prothprm  47902  tgblthelfgott  48098  tgoldbachlt  48099  nnlog2ge0lt1  48849  1aryenefmnd  48929  ackval42  48979