Theorem breqtrri 5129

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

Syntax hints:   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  3brtr4i  5132  ensn1  9004  1sdom2ALT  9195  dju1p1e2ALT  10133  infmap2  10175  0lt1sr  11055  0le2OLD  12323  2posOLD  12325  1lt2  12392  2lt3  12393  3lt4  12396  4lt5  12399  5lt6  12403  6lt7  12408  7lt8  12414  8lt9  12421  numltc  12721  declti  12733  xlemul1a  13293  sqge0i  14203  faclbnd2  14306  cats1fv  14874  ege2le3  16122  cos2bnd  16222  3dvdsdec  16368  n2dvdsm1  16405  sumeven  16423  divalglem2  16431  pockthi  16945  dec2dvds  17101  prmlem1  17145  prmlem2  17158  1259prm  17174  2503prm  17178  4001prm  17183  vitalilem5  25676  dveflem  26043  tangtx  26572  sinq12ge0  26575  logi  26654  cxpge0  26750  asin1  26961  birthday  27021  lgamgulmlem4  27098  ppiub  27270  bposlem7  27356  lgsdir2lem2  27392  pthdlem2  29970  ex-fl  30651  ex-ind-dvds  30665  siilem2  31057  normlem6  31320  normlem7  31321  cm2mi  31831  pjnormi  31926  unierri  32309  dp2lt10  33063  dpgti  33085  pfx1s2  33119  cyc2fv2  33304  cyc3fv3  33321  hgt750lemd  34944  hgt750lem  34947  hgt750lem2  34948  hgt750leme  34954  cnndvlem1  36980  taupi  37820  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  ftc1anclem5  38201  fdc  38249  lcmineqlem23  42673  3lexlogpow2ineq2  42681  pellfundgt1  43465  jm2.27dlem2  43592  stoweidlem13  46592  sqwvfoura  46807  sqwvfourb  46808  fourierswlem  46809  goldrapos  47482  m1modnep2mod  47957  41prothprm  48233  nprmdvdsfacm1lem4  48237  tgblthelfgott  48442  tgoldbachlt  48443  nnlog2ge0lt1  49193  1aryenefmnd  49273  ackval42  49323