Theorem breqtrri 5129

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

Syntax hints:   = wceq 1540   class class class wbr 5102

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  3brtr4i  5132  ensn1  8969  1sdom2ALT  9165  dju1p1e2ALT  10106  infmap2  10148  0lt1sr  11026  0le2  12266  2pos  12267  3pos  12269  4pos  12271  5pos  12273  6pos  12274  7pos  12275  8pos  12276  9pos  12277  1lt2  12330  2lt3  12331  3lt4  12333  4lt5  12336  5lt6  12340  6lt7  12345  7lt8  12351  8lt9  12358  numltc  12653  declti  12665  xlemul1a  13226  sqge0i  14131  faclbnd2  14234  cats1fv  14802  ege2le3  16033  cos2bnd  16133  3dvdsdec  16279  n2dvdsm1  16316  sumeven  16334  divalglem2  16342  pockthi  16855  dec2dvds  17011  prmlem1  17055  prmlem2  17067  1259prm  17083  2503prm  17087  4001prm  17092  vitalilem5  25547  dveflem  25917  tangtx  26448  sinq12ge0  26451  logi  26530  cxpge0  26626  asin1  26838  birthday  26898  lgamgulmlem4  26976  ppiub  27149  bposlem7  27235  lgsdir2lem2  27271  pthdlem2  29749  ex-fl  30427  ex-ind-dvds  30441  siilem2  30832  normlem6  31095  normlem7  31096  cm2mi  31606  pjnormi  31701  unierri  32084  dp2lt10  32855  dpgti  32877  pfx1s2  32911  cyc2fv2  33095  cyc3fv3  33112  hgt750lemd  34633  hgt750lem  34636  hgt750lem2  34637  hgt750leme  34643  cnndvlem1  36519  taupi  37305  poimirlem25  37633  poimirlem26  37634  poimirlem27  37635  poimirlem28  37636  ftc1anclem5  37685  fdc  37733  lcmineqlem23  42033  3lexlogpow2ineq2  42041  pellfundgt1  42865  jm2.27dlem2  42993  stoweidlem13  46005  sqwvfoura  46220  sqwvfourb  46221  fourierswlem  46222  tworepnotupword  46878  m1modnep2mod  47347  41prothprm  47614  tgblthelfgott  47810  tgoldbachlt  47811  nnlog2ge0lt1  48549  1aryenefmnd  48629  ackval42  48679