Theorem breqtrri 5174

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

Syntax hints:   = wceq 1541   class class class wbr 5147

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  3brtr4i  5177  ensn1  9013  ensn1OLD  9014  1sdom2ALT  9237  dju1p1e2ALT  10165  infmap2  10209  0lt1sr  11086  0le2  12310  2pos  12311  3pos  12313  4pos  12315  5pos  12317  6pos  12318  7pos  12319  8pos  12320  9pos  12321  1lt2  12379  2lt3  12380  3lt4  12382  4lt5  12385  5lt6  12389  6lt7  12394  7lt8  12400  8lt9  12407  nn0le2xi  12522  numltc  12699  declti  12711  xlemul1a  13263  sqge0i  14148  faclbnd2  14247  cats1fv  14806  ege2le3  16029  cos2bnd  16127  3dvdsdec  16271  n2dvdsm1  16308  sumeven  16326  divalglem2  16334  pockthi  16836  dec2dvds  16992  prmlem1  17037  prmlem2  17049  1259prm  17065  2503prm  17069  4001prm  17074  2strstr1OLD  17166  vitalilem5  25120  dveflem  25487  tangtx  26006  sinq12ge0  26009  cxpge0  26182  asin1  26388  birthday  26448  lgamgulmlem4  26525  ppiub  26696  bposlem7  26782  lgsdir2lem2  26818  pthdlem2  29014  ex-fl  29689  ex-ind-dvds  29703  siilem2  30092  normlem6  30355  normlem7  30356  cm2mi  30866  pjnormi  30961  unierri  31344  dp2lt10  32037  dpgti  32059  pfx1s2  32092  cyc2fv2  32268  cyc3fv3  32285  hgt750lemd  33648  hgt750lem  33651  hgt750lem2  33652  hgt750leme  33658  logi  34692  cnndvlem1  35401  taupi  36192  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  ftc1anclem5  36553  fdc  36601  lcmineqlem23  40904  3lexlogpow2ineq2  40912  pellfundgt1  41606  jm2.27dlem2  41734  stoweidlem13  44715  sqwvfoura  44930  sqwvfourb  44931  fourierswlem  44932  tworepnotupword  45586  41prothprm  46273  tgblthelfgott  46469  tgoldbachlt  46470  nnlog2ge0lt1  47205  1aryenefmnd  47285  ackval42  47335