Theorem breqtrri 5170

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

Syntax hints:   = wceq 1540   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  3brtr4i  5173  ensn1  9061  1sdom2ALT  9277  dju1p1e2ALT  10215  infmap2  10257  0lt1sr  11135  0le2  12368  2pos  12369  3pos  12371  4pos  12373  5pos  12375  6pos  12376  7pos  12377  8pos  12378  9pos  12379  1lt2  12437  2lt3  12438  3lt4  12440  4lt5  12443  5lt6  12447  6lt7  12452  7lt8  12458  8lt9  12465  numltc  12759  declti  12771  xlemul1a  13330  sqge0i  14227  faclbnd2  14330  cats1fv  14898  ege2le3  16126  cos2bnd  16224  3dvdsdec  16369  n2dvdsm1  16406  sumeven  16424  divalglem2  16432  pockthi  16945  dec2dvds  17101  prmlem1  17145  prmlem2  17157  1259prm  17173  2503prm  17177  4001prm  17182  2strstr1OLD  17271  vitalilem5  25647  dveflem  26017  tangtx  26547  sinq12ge0  26550  logi  26629  cxpge0  26725  asin1  26937  birthday  26997  lgamgulmlem4  27075  ppiub  27248  bposlem7  27334  lgsdir2lem2  27370  n0scut  28338  pthdlem2  29788  ex-fl  30466  ex-ind-dvds  30480  siilem2  30871  normlem6  31134  normlem7  31135  cm2mi  31645  pjnormi  31740  unierri  32123  dp2lt10  32866  dpgti  32888  pfx1s2  32923  cyc2fv2  33142  cyc3fv3  33159  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  cnndvlem1  36538  taupi  37324  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  ftc1anclem5  37704  fdc  37752  lcmineqlem23  42052  3lexlogpow2ineq2  42060  pellfundgt1  42894  jm2.27dlem2  43022  stoweidlem13  46028  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  tworepnotupword  46901  m1modnep2mod  47354  41prothprm  47606  tgblthelfgott  47802  tgoldbachlt  47803  nnlog2ge0lt1  48487  1aryenefmnd  48567  ackval42  48617