Theorem breqtrri 5175

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

Syntax hints:   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  3brtr4i  5178  ensn1  9060  1sdom2ALT  9275  dju1p1e2ALT  10213  infmap2  10255  0lt1sr  11133  0le2  12366  2pos  12367  3pos  12369  4pos  12371  5pos  12373  6pos  12374  7pos  12375  8pos  12376  9pos  12377  1lt2  12435  2lt3  12436  3lt4  12438  4lt5  12441  5lt6  12445  6lt7  12450  7lt8  12456  8lt9  12463  numltc  12757  declti  12769  xlemul1a  13327  sqge0i  14224  faclbnd2  14327  cats1fv  14895  ege2le3  16123  cos2bnd  16221  3dvdsdec  16366  n2dvdsm1  16403  sumeven  16421  divalglem2  16429  pockthi  16941  dec2dvds  17097  prmlem1  17142  prmlem2  17154  1259prm  17170  2503prm  17174  4001prm  17179  2strstr1OLD  17271  vitalilem5  25661  dveflem  26032  tangtx  26562  sinq12ge0  26565  logi  26644  cxpge0  26740  asin1  26952  birthday  27012  lgamgulmlem4  27090  ppiub  27263  bposlem7  27349  lgsdir2lem2  27385  n0scut  28353  pthdlem2  29801  ex-fl  30476  ex-ind-dvds  30490  siilem2  30881  normlem6  31144  normlem7  31145  cm2mi  31655  pjnormi  31750  unierri  32133  dp2lt10  32851  dpgti  32873  pfx1s2  32908  cyc2fv2  33125  cyc3fv3  33142  hgt750lemd  34642  hgt750lem  34645  hgt750lem2  34646  hgt750leme  34652  cnndvlem1  36520  taupi  37306  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  ftc1anclem5  37684  fdc  37732  lcmineqlem23  42033  3lexlogpow2ineq2  42041  pellfundgt1  42871  jm2.27dlem2  42999  stoweidlem13  45969  sqwvfoura  46184  sqwvfourb  46185  fourierswlem  46186  tworepnotupword  46840  m1modnep2mod  47292  41prothprm  47544  tgblthelfgott  47740  tgoldbachlt  47741  nnlog2ge0lt1  48416  1aryenefmnd  48496  ackval42  48546