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

Syntax hints:   = wceq 1539   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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  3brtr4i  5105  ensn1  8816  ensn1OLD  8817  1sdom2  9030  dju1p1e2ALT  9939  infmap2  9983  0lt1sr  10860  0le2  12084  2pos  12085  3pos  12087  4pos  12089  5pos  12091  6pos  12092  7pos  12093  8pos  12094  9pos  12095  1lt2  12153  2lt3  12154  3lt4  12156  4lt5  12159  5lt6  12163  6lt7  12168  7lt8  12174  8lt9  12181  nn0le2xi  12296  numltc  12472  declti  12484  xlemul1a  13031  sqge0i  13914  faclbnd2  14014  cats1fv  14581  ege2le3  15808  cos2bnd  15906  3dvdsdec  16050  n2dvdsm1  16087  sumeven  16105  divalglem2  16113  pockthi  16617  dec2dvds  16773  prmlem1  16818  prmlem2  16830  1259prm  16846  2503prm  16850  4001prm  16855  2strstr1OLD  16947  vitalilem5  24785  dveflem  25152  tangtx  25671  sinq12ge0  25674  cxpge0  25847  asin1  26053  birthday  26113  lgamgulmlem4  26190  ppiub  26361  bposlem7  26447  lgsdir2lem2  26483  pthdlem2  28145  ex-fl  28820  ex-ind-dvds  28834  siilem2  29223  normlem6  29486  normlem7  29487  cm2mi  29997  pjnormi  30092  unierri  30475  dp2lt10  31167  dpgti  31189  pfx1s2  31222  cyc2fv2  31398  cyc3fv3  31415  hgt750lemd  32637  hgt750lem  32640  hgt750lem2  32641  hgt750leme  32647  logi  33709  cnndvlem1  34726  taupi  35503  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  ftc1anclem5  35863  fdc  35912  lcmineqlem23  40066  3lexlogpow2ineq2  40074  pellfundgt1  40712  jm2.27dlem2  40839  stoweidlem13  43561  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  41prothprm  45082  tgblthelfgott  45278  tgoldbachlt  45279  nnlog2ge0lt1  45923  1aryenefmnd  46003  ackval42  46053  tworepnotupword  46532