Theorem breqtrri 5119

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

Syntax hints:   = wceq 1540   class class class wbr 5092

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  3brtr4i  5122  ensn1  8946  1sdom2ALT  9138  dju1p1e2ALT  10069  infmap2  10111  0lt1sr  10989  0le2  12230  2pos  12231  3pos  12233  4pos  12235  5pos  12237  6pos  12238  7pos  12239  8pos  12240  9pos  12241  1lt2  12294  2lt3  12295  3lt4  12297  4lt5  12300  5lt6  12304  6lt7  12309  7lt8  12315  8lt9  12322  numltc  12617  declti  12629  xlemul1a  13190  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  25511  dveflem  25881  tangtx  26412  sinq12ge0  26415  logi  26494  cxpge0  26590  asin1  26802  birthday  26862  lgamgulmlem4  26940  ppiub  27113  bposlem7  27199  lgsdir2lem2  27235  pthdlem2  29717  ex-fl  30395  ex-ind-dvds  30409  siilem2  30800  normlem6  31063  normlem7  31064  cm2mi  31574  pjnormi  31669  unierri  32052  dp2lt10  32833  dpgti  32855  pfx1s2  32889  cyc2fv2  33073  cyc3fv3  33090  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  cnndvlem1  36531  taupi  37317  poimirlem25  37645  poimirlem26  37646  poimirlem27  37647  poimirlem28  37648  ftc1anclem5  37697  fdc  37745  lcmineqlem23  42044  3lexlogpow2ineq2  42052  pellfundgt1  42876  jm2.27dlem2  43003  stoweidlem13  46014  sqwvfoura  46229  sqwvfourb  46230  fourierswlem  46231  tworepnotupword  46887  m1modnep2mod  47356  41prothprm  47623  tgblthelfgott  47819  tgoldbachlt  47820  nnlog2ge0lt1  48571  1aryenefmnd  48651  ackval42  48701