Theorem breqtrri 5126

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

Syntax hints:   = wceq 1542   class class class wbr 5099

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  3brtr4i  5129  ensn1  8962  1sdom2ALT  9153  dju1p1e2ALT  10089  infmap2  10131  0lt1sr  11010  0le2  12251  2pos  12252  3pos  12254  4pos  12256  5pos  12258  6pos  12259  7pos  12260  8pos  12261  9pos  12262  1lt2  12315  2lt3  12316  3lt4  12318  4lt5  12321  5lt6  12325  6lt7  12330  7lt8  12336  8lt9  12343  numltc  12637  declti  12649  xlemul1a  13207  sqge0i  14115  faclbnd2  14218  cats1fv  14786  ege2le3  16017  cos2bnd  16117  3dvdsdec  16263  n2dvdsm1  16300  sumeven  16318  divalglem2  16326  pockthi  16839  dec2dvds  16995  prmlem1  17039  prmlem2  17051  1259prm  17067  2503prm  17071  4001prm  17076  vitalilem5  25573  dveflem  25943  tangtx  26474  sinq12ge0  26477  logi  26556  cxpge0  26652  asin1  26864  birthday  26924  lgamgulmlem4  27002  ppiub  27175  bposlem7  27261  lgsdir2lem2  27297  pthdlem2  29845  ex-fl  30526  ex-ind-dvds  30540  siilem2  30931  normlem6  31194  normlem7  31195  cm2mi  31705  pjnormi  31800  unierri  32183  dp2lt10  32967  dpgti  32989  pfx1s2  33023  cyc2fv2  33206  cyc3fv3  33223  hgt750lemd  34807  hgt750lem  34810  hgt750lem2  34811  hgt750leme  34817  cnndvlem1  36739  taupi  37530  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  ftc1anclem5  37900  fdc  37948  lcmineqlem23  42373  3lexlogpow2ineq2  42381  pellfundgt1  43192  jm2.27dlem2  43319  stoweidlem13  46324  sqwvfoura  46539  sqwvfourb  46540  fourierswlem  46541  m1modnep2mod  47665  41prothprm  47932  tgblthelfgott  48128  tgoldbachlt  48129  nnlog2ge0lt1  48879  1aryenefmnd  48959  ackval42  49009