Theorem breqtrri 5113

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 5111	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5086

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  3brtr4i  5116  ensn1  8963  1sdom2ALT  9154  dju1p1e2ALT  10092  infmap2  10134  0lt1sr  11013  0le2  12278  2pos  12279  3pos  12281  4pos  12283  5pos  12285  6pos  12286  7pos  12287  8pos  12288  9pos  12289  1lt2  12342  2lt3  12343  3lt4  12345  4lt5  12348  5lt6  12352  6lt7  12357  7lt8  12363  8lt9  12370  numltc  12665  declti  12677  xlemul1a  13235  sqge0i  14145  faclbnd2  14248  cats1fv  14816  ege2le3  16050  cos2bnd  16150  3dvdsdec  16296  n2dvdsm1  16333  sumeven  16351  divalglem2  16359  pockthi  16873  dec2dvds  17029  prmlem1  17073  prmlem2  17085  1259prm  17101  2503prm  17105  4001prm  17110  vitalilem5  25593  dveflem  25960  tangtx  26486  sinq12ge0  26489  logi  26568  cxpge0  26664  asin1  26875  birthday  26935  lgamgulmlem4  27013  ppiub  27185  bposlem7  27271  lgsdir2lem2  27307  pthdlem2  29855  ex-fl  30536  ex-ind-dvds  30550  siilem2  30942  normlem6  31205  normlem7  31206  cm2mi  31716  pjnormi  31811  unierri  32194  dp2lt10  32962  dpgti  32984  pfx1s2  33018  cyc2fv2  33202  cyc3fv3  33219  hgt750lemd  34812  hgt750lem  34815  hgt750lem2  34816  hgt750leme  34822  cnndvlem1  36817  taupi  37657  poimirlem25  37986  poimirlem26  37987  poimirlem27  37988  poimirlem28  37989  ftc1anclem5  38038  fdc  38086  lcmineqlem23  42510  3lexlogpow2ineq2  42518  pellfundgt1  43335  jm2.27dlem2  43462  stoweidlem13  46465  sqwvfoura  46680  sqwvfourb  46681  fourierswlem  46682  goldrapos  47351  m1modnep2mod  47824  41prothprm  48100  nprmdvdsfacm1lem4  48104  tgblthelfgott  48309  tgoldbachlt  48310  nnlog2ge0lt1  49060  1aryenefmnd  49140  ackval42  49190