Theorem breqtrri 5176

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

Syntax hints:   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  3brtr4i  5179  ensn1  9017  ensn1OLD  9018  1sdom2ALT  9241  dju1p1e2ALT  10169  infmap2  10213  0lt1sr  11090  0le2  12314  2pos  12315  3pos  12317  4pos  12319  5pos  12321  6pos  12322  7pos  12323  8pos  12324  9pos  12325  1lt2  12383  2lt3  12384  3lt4  12386  4lt5  12389  5lt6  12393  6lt7  12398  7lt8  12404  8lt9  12411  nn0le2xi  12526  numltc  12703  declti  12715  xlemul1a  13267  sqge0i  14152  faclbnd2  14251  cats1fv  14810  ege2le3  16033  cos2bnd  16131  3dvdsdec  16275  n2dvdsm1  16312  sumeven  16330  divalglem2  16338  pockthi  16840  dec2dvds  16996  prmlem1  17041  prmlem2  17053  1259prm  17069  2503prm  17073  4001prm  17078  2strstr1OLD  17170  vitalilem5  25129  dveflem  25496  tangtx  26015  sinq12ge0  26018  cxpge0  26191  asin1  26399  birthday  26459  lgamgulmlem4  26536  ppiub  26707  bposlem7  26793  lgsdir2lem2  26829  pthdlem2  29025  ex-fl  29700  ex-ind-dvds  29714  siilem2  30105  normlem6  30368  normlem7  30369  cm2mi  30879  pjnormi  30974  unierri  31357  dp2lt10  32050  dpgti  32072  pfx1s2  32105  cyc2fv2  32281  cyc3fv3  32298  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  logi  34704  cnndvlem1  35413  taupi  36204  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  ftc1anclem5  36565  fdc  36613  lcmineqlem23  40916  3lexlogpow2ineq2  40924  pellfundgt1  41621  jm2.27dlem2  41749  stoweidlem13  44729  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  tworepnotupword  45600  41prothprm  46287  tgblthelfgott  46483  tgoldbachlt  46484  nnlog2ge0lt1  47252  1aryenefmnd  47332  ackval42  47382