Theorem breqtrri 5127

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

Syntax hints:   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  3brtr4i  5130  ensn1  8972  1sdom2ALT  9163  dju1p1e2ALT  10099  infmap2  10141  0lt1sr  11020  0le2  12261  2pos  12262  3pos  12264  4pos  12266  5pos  12268  6pos  12269  7pos  12270  8pos  12271  9pos  12272  1lt2  12325  2lt3  12326  3lt4  12328  4lt5  12331  5lt6  12335  6lt7  12340  7lt8  12346  8lt9  12353  numltc  12647  declti  12659  xlemul1a  13217  sqge0i  14125  faclbnd2  14228  cats1fv  14796  ege2le3  16027  cos2bnd  16127  3dvdsdec  16273  n2dvdsm1  16310  sumeven  16328  divalglem2  16336  pockthi  16849  dec2dvds  17005  prmlem1  17049  prmlem2  17061  1259prm  17077  2503prm  17081  4001prm  17086  vitalilem5  25586  dveflem  25956  tangtx  26487  sinq12ge0  26490  logi  26569  cxpge0  26665  asin1  26877  birthday  26937  lgamgulmlem4  27015  ppiub  27188  bposlem7  27274  lgsdir2lem2  27310  pthdlem2  29859  ex-fl  30540  ex-ind-dvds  30554  siilem2  30946  normlem6  31209  normlem7  31210  cm2mi  31720  pjnormi  31815  unierri  32198  dp2lt10  32982  dpgti  33004  pfx1s2  33038  cyc2fv2  33222  cyc3fv3  33239  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  cnndvlem1  36765  taupi  37605  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  ftc1anclem5  37977  fdc  38025  lcmineqlem23  42450  3lexlogpow2ineq2  42458  pellfundgt1  43269  jm2.27dlem2  43396  stoweidlem13  46400  sqwvfoura  46615  sqwvfourb  46616  fourierswlem  46617  m1modnep2mod  47741  41prothprm  48008  tgblthelfgott  48204  tgoldbachlt  48205  nnlog2ge0lt1  48955  1aryenefmnd  49035  ackval42  49085