Theorem breqtrri 5136

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 5134	1 ⊢ 𝐴𝑅𝐶

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  3brtr4i  5139  ensn1  9031  1sdom2ALT  9223  dju1p1e2ALT  10181  infmap2  10223  0lt1sr  11108  0le2OLD  12372  2posOLD  12374  1lt2  12441  2lt3  12442  3lt4  12445  4lt5  12448  5lt6  12452  6lt7  12457  7lt8  12463  8lt9  12470  numltc  12771  declti  12783  xlemul1a  13344  sqge0i  14256  faclbnd2  14359  cats1fv  14934  ege2le3  16182  cos2bnd  16282  3dvdsdec  16428  n2dvdsm1  16465  sumeven  16483  divalglem2  16491  pockthi  17005  dec2dvds  17161  prmlem1  17205  prmlem2  17218  1259prm  17234  2503prm  17238  4001prm  17243  vitalilem5  25846  dveflem  26213  tangtx  26750  sinq12ge0  26753  logi  26832  cxpge0  26928  asin1  27139  birthday  27199  lgamgulmlem4  27276  ppiub  27448  bposlem7  27534  lgsdir2lem2  27570  pthdlem2  30241  ex-fl  30935  ex-ind-dvds  30949  siilem2  31341  normlem6  31604  normlem7  31605  cm2mi  32115  pjnormi  32210  unierri  32593  dp2lt10  33337  dpgti  33359  pfx1s2  33393  cyc2fv2  33570  cyc3fv3  33587  hgt750lemd  35164  hgt750lem  35167  hgt750lem2  35168  hgt750leme  35174  cnndvlem1  37242  taupi  38083  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  ftc1anclem5  38454  fdc  38503  lcmineqlem23  42925  3lexlogpow2ineq2  42933  pellfundgt1  43732  jm2.27dlem2  43859  stoweidlem13  46849  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  goldrapos  47756  goldratval  47762  sinnpoly  47767  m1modnep2mod  48254  41prothprm  48530  nprmdvdsfacm1lem4  48534  tgblthelfgott  48739  tgoldbachlt  48740  nnlog2ge0lt1  49504  1aryenefmnd  49584  ackval42  49634