Theorem breqtrri 5193

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

Syntax hints:   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  3brtr4i  5196  ensn1  9082  ensn1OLD  9083  1sdom2ALT  9304  dju1p1e2ALT  10244  infmap2  10286  0lt1sr  11164  0le2  12395  2pos  12396  3pos  12398  4pos  12400  5pos  12402  6pos  12403  7pos  12404  8pos  12405  9pos  12406  1lt2  12464  2lt3  12465  3lt4  12467  4lt5  12470  5lt6  12474  6lt7  12479  7lt8  12485  8lt9  12492  nn0le2xi  12607  numltc  12784  declti  12796  xlemul1a  13350  sqge0i  14237  faclbnd2  14340  cats1fv  14908  ege2le3  16138  cos2bnd  16236  3dvdsdec  16380  n2dvdsm1  16417  sumeven  16435  divalglem2  16443  pockthi  16954  dec2dvds  17110  prmlem1  17155  prmlem2  17167  1259prm  17183  2503prm  17187  4001prm  17192  2strstr1OLD  17284  vitalilem5  25666  dveflem  26037  tangtx  26565  sinq12ge0  26568  logi  26647  cxpge0  26743  asin1  26955  birthday  27015  lgamgulmlem4  27093  ppiub  27266  bposlem7  27352  lgsdir2lem2  27388  n0scut  28356  pthdlem2  29804  ex-fl  30479  ex-ind-dvds  30493  siilem2  30884  normlem6  31147  normlem7  31148  cm2mi  31658  pjnormi  31753  unierri  32136  dp2lt10  32848  dpgti  32870  pfx1s2  32905  cyc2fv2  33115  cyc3fv3  33132  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  cnndvlem1  36503  taupi  37289  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  ftc1anclem5  37657  fdc  37705  lcmineqlem23  42008  3lexlogpow2ineq2  42016  pellfundgt1  42839  jm2.27dlem2  42967  stoweidlem13  45934  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  tworepnotupword  46805  41prothprm  47493  tgblthelfgott  47689  tgoldbachlt  47690  nnlog2ge0lt1  48300  1aryenefmnd  48380  ackval42  48430