Theorem breqtrri 5134

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

Syntax hints:   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  3brtr4i  5137  ensn1  8992  1sdom2ALT  9188  dju1p1e2ALT  10128  infmap2  10170  0lt1sr  11048  0le2  12288  2pos  12289  3pos  12291  4pos  12293  5pos  12295  6pos  12296  7pos  12297  8pos  12298  9pos  12299  1lt2  12352  2lt3  12353  3lt4  12355  4lt5  12358  5lt6  12362  6lt7  12367  7lt8  12373  8lt9  12380  numltc  12675  declti  12687  xlemul1a  13248  sqge0i  14153  faclbnd2  14256  cats1fv  14825  ege2le3  16056  cos2bnd  16156  3dvdsdec  16302  n2dvdsm1  16339  sumeven  16357  divalglem2  16365  pockthi  16878  dec2dvds  17034  prmlem1  17078  prmlem2  17090  1259prm  17106  2503prm  17110  4001prm  17115  vitalilem5  25513  dveflem  25883  tangtx  26414  sinq12ge0  26417  logi  26496  cxpge0  26592  asin1  26804  birthday  26864  lgamgulmlem4  26942  ppiub  27115  bposlem7  27201  lgsdir2lem2  27237  pthdlem2  29698  ex-fl  30376  ex-ind-dvds  30390  siilem2  30781  normlem6  31044  normlem7  31045  cm2mi  31555  pjnormi  31650  unierri  32033  dp2lt10  32804  dpgti  32826  pfx1s2  32860  cyc2fv2  33079  cyc3fv3  33096  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  cnndvlem1  36525  taupi  37311  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  ftc1anclem5  37691  fdc  37739  lcmineqlem23  42039  3lexlogpow2ineq2  42047  pellfundgt1  42871  jm2.27dlem2  42999  stoweidlem13  46011  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  tworepnotupword  46884  m1modnep2mod  47353  41prothprm  47620  tgblthelfgott  47816  tgoldbachlt  47817  nnlog2ge0lt1  48555  1aryenefmnd  48635  ackval42  48685