Theorem breqtrri 5112

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

Syntax hints:   = wceq 1542   class class class wbr 5085

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  3brtr4i  5115  ensn1  8968  1sdom2ALT  9159  dju1p1e2ALT  10097  infmap2  10139  0lt1sr  11018  0le2  12283  2pos  12284  3pos  12286  4pos  12288  5pos  12290  6pos  12291  7pos  12292  8pos  12293  9pos  12294  1lt2  12347  2lt3  12348  3lt4  12350  4lt5  12353  5lt6  12357  6lt7  12362  7lt8  12368  8lt9  12375  numltc  12670  declti  12682  xlemul1a  13240  sqge0i  14150  faclbnd2  14253  cats1fv  14821  ege2le3  16055  cos2bnd  16155  3dvdsdec  16301  n2dvdsm1  16338  sumeven  16356  divalglem2  16364  pockthi  16878  dec2dvds  17034  prmlem1  17078  prmlem2  17090  1259prm  17106  2503prm  17110  4001prm  17115  vitalilem5  25579  dveflem  25946  tangtx  26469  sinq12ge0  26472  logi  26551  cxpge0  26647  asin1  26858  birthday  26918  lgamgulmlem4  26995  ppiub  27167  bposlem7  27253  lgsdir2lem2  27289  pthdlem2  29836  ex-fl  30517  ex-ind-dvds  30531  siilem2  30923  normlem6  31186  normlem7  31187  cm2mi  31697  pjnormi  31792  unierri  32175  dp2lt10  32943  dpgti  32965  pfx1s2  32999  cyc2fv2  33183  cyc3fv3  33200  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  cnndvlem1  36797  taupi  37637  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  ftc1anclem5  38018  fdc  38066  lcmineqlem23  42490  3lexlogpow2ineq2  42498  pellfundgt1  43311  jm2.27dlem2  43438  stoweidlem13  46441  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  goldrapos  47331  m1modnep2mod  47806  41prothprm  48082  nprmdvdsfacm1lem4  48086  tgblthelfgott  48291  tgoldbachlt  48292  nnlog2ge0lt1  49042  1aryenefmnd  49122  ackval42  49172