Theorem breqtrri 5102

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

Syntax hints:   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  3brtr4i  5105  ensn1  8962  1sdom2ALT  9153  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  25601  dveflem  25968  tangtx  26491  sinq12ge0  26494  logi  26573  cxpge0  26669  asin1  26880  birthday  26940  lgamgulmlem4  27017  ppiub  27189  bposlem7  27275  lgsdir2lem2  27311  pthdlem2  29858  ex-fl  30539  ex-ind-dvds  30553  siilem2  30945  normlem6  31208  normlem7  31209  cm2mi  31719  pjnormi  31814  unierri  32197  dp2lt10  32966  dpgti  32988  pfx1s2  33022  cyc2fv2  33207  cyc3fv3  33224  hgt750lemd  34844  hgt750lem  34847  hgt750lem2  34848  hgt750leme  34854  cnndvlem1  36858  taupi  37698  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  poimirlem28  38030  ftc1anclem5  38079  fdc  38127  lcmineqlem23  42551  3lexlogpow2ineq2  42559  pellfundgt1  43343  jm2.27dlem2  43470  stoweidlem13  46470  sqwvfoura  46685  sqwvfourb  46686  fourierswlem  46687  goldrapos  47360  m1modnep2mod  47835  41prothprm  48111  nprmdvdsfacm1lem4  48115  tgblthelfgott  48320  tgoldbachlt  48321  nnlog2ge0lt1  49071  1aryenefmnd  49151  ackval42  49201