Theorem breqtrri 5137

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  3brtr4i  5140  ensn1  9016  1sdom2ALT  9207  dju1p1e2ALT  10165  infmap2  10207  0lt1sr  11086  0le2OLD  12350  2posOLD  12352  1lt2  12419  2lt3  12420  3lt4  12423  4lt5  12426  5lt6  12430  6lt7  12435  7lt8  12441  8lt9  12448  numltc  12748  declti  12760  xlemul1a  13320  sqge0i  14231  faclbnd2  14334  cats1fv  14903  ege2le3  16150  cos2bnd  16250  3dvdsdec  16396  n2dvdsm1  16433  sumeven  16451  divalglem2  16459  pockthi  16973  dec2dvds  17129  prmlem1  17173  prmlem2  17186  1259prm  17202  2503prm  17206  4001prm  17211  vitalilem5  25782  dveflem  26149  tangtx  26681  sinq12ge0  26684  logi  26763  cxpge0  26859  asin1  27070  birthday  27130  lgamgulmlem4  27207  ppiub  27379  bposlem7  27465  lgsdir2lem2  27501  pthdlem2  30128  ex-fl  30809  ex-ind-dvds  30823  siilem2  31215  normlem6  31478  normlem7  31479  cm2mi  31989  pjnormi  32084  unierri  32467  dp2lt10  33214  dpgti  33236  pfx1s2  33270  cyc2fv2  33451  cyc3fv3  33468  hgt750lemd  35044  hgt750lem  35047  hgt750lem2  35048  hgt750leme  35054  cnndvlem1  37154  taupi  37995  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  ftc1anclem5  38376  fdc  38424  lcmineqlem23  42846  3lexlogpow2ineq2  42854  pellfundgt1  43638  jm2.27dlem2  43765  stoweidlem13  46755  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  goldrapos  47648  m1modnep2mod  48123  41prothprm  48399  nprmdvdsfacm1lem4  48403  tgblthelfgott  48608  tgoldbachlt  48609  nnlog2ge0lt1  49374  1aryenefmnd  49454  ackval42  49504