Theorem breqtrri 5140

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

Syntax hints:   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  3brtr4i  5143  ensn1  9018  1sdom2ALT  9209  dju1p1e2ALT  10158  infmap2  10200  0lt1sr  11080  0le2OLD  12344  2posOLD  12346  1lt2  12413  2lt3  12414  3lt4  12417  4lt5  12420  5lt6  12424  6lt7  12429  7lt8  12435  8lt9  12442  numltc  12742  declti  12754  xlemul1a  13314  sqge0i  14224  faclbnd2  14327  cats1fv  14896  ege2le3  16144  cos2bnd  16244  3dvdsdec  16390  n2dvdsm1  16427  sumeven  16445  divalglem2  16453  pockthi  16967  dec2dvds  17123  prmlem1  17167  prmlem2  17180  1259prm  17196  2503prm  17200  4001prm  17205  vitalilem5  25740  dveflem  26107  tangtx  26636  sinq12ge0  26639  logi  26718  cxpge0  26814  asin1  27025  birthday  27085  lgamgulmlem4  27162  ppiub  27334  bposlem7  27420  lgsdir2lem2  27456  pthdlem2  30058  ex-fl  30739  ex-ind-dvds  30753  siilem2  31145  normlem6  31408  normlem7  31409  cm2mi  31919  pjnormi  32014  unierri  32397  dp2lt10  33144  dpgti  33166  pfx1s2  33200  cyc2fv2  33383  cyc3fv3  33400  hgt750lemd  34980  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  cnndvlem1  37049  taupi  37890  poimirlem25  38219  poimirlem26  38220  poimirlem27  38221  poimirlem28  38222  ftc1anclem5  38271  fdc  38319  lcmineqlem23  42743  3lexlogpow2ineq2  42751  pellfundgt1  43537  jm2.27dlem2  43664  stoweidlem13  46654  sqwvfoura  46869  sqwvfourb  46870  fourierswlem  46871  goldrapos  47544  m1modnep2mod  48019  41prothprm  48295  nprmdvdsfacm1lem4  48299  tgblthelfgott  48504  tgoldbachlt  48505  nnlog2ge0lt1  49266  1aryenefmnd  49346  ackval42  49396