Theorem breqtrri 5097

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

Syntax hints:   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  3brtr4i  5100  ensn1  8761  ensn1OLD  8762  1sdom2  8951  dju1p1e2ALT  9861  infmap2  9905  0lt1sr  10782  0le2  12005  2pos  12006  3pos  12008  4pos  12010  5pos  12012  6pos  12013  7pos  12014  8pos  12015  9pos  12016  1lt2  12074  2lt3  12075  3lt4  12077  4lt5  12080  5lt6  12084  6lt7  12089  7lt8  12095  8lt9  12102  nn0le2xi  12217  numltc  12392  declti  12404  xlemul1a  12951  sqge0i  13833  faclbnd2  13933  cats1fv  14500  ege2le3  15727  cos2bnd  15825  3dvdsdec  15969  n2dvdsm1  16006  sumeven  16024  divalglem2  16032  pockthi  16536  dec2dvds  16692  prmlem1  16737  prmlem2  16749  1259prm  16765  2503prm  16769  4001prm  16774  2strstr1OLD  16864  vitalilem5  24681  dveflem  25048  tangtx  25567  sinq12ge0  25570  cxpge0  25743  asin1  25949  birthday  26009  lgamgulmlem4  26086  ppiub  26257  bposlem7  26343  lgsdir2lem2  26379  pthdlem2  28037  ex-fl  28712  ex-ind-dvds  28726  siilem2  29115  normlem6  29378  normlem7  29379  cm2mi  29889  pjnormi  29984  unierri  30367  dp2lt10  31060  dpgti  31082  pfx1s2  31115  cyc2fv2  31291  cyc3fv3  31308  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  logi  33606  cnndvlem1  34644  taupi  35421  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  ftc1anclem5  35781  fdc  35830  lcmineqlem23  39987  3lexlogpow2ineq2  39995  pellfundgt1  40621  jm2.27dlem2  40748  stoweidlem13  43444  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  41prothprm  44959  tgblthelfgott  45155  tgoldbachlt  45156  nnlog2ge0lt1  45800  1aryenefmnd  45880  ackval42  45930