Theorem breqtrri 5132

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  3brtr4i  5135  ensn1  9027  1sdom2ALT  9219  dju1p1e2ALT  10210  infmap2  10252  0lt1sr  11137  0le2OLD  12401  2posOLD  12403  1lt2  12470  2lt3  12471  3lt4  12474  4lt5  12477  5lt6  12481  6lt7  12486  7lt8  12492  8lt9  12499  numltc  12800  declti  12812  xlemul1a  13373  sqge0i  14285  faclbnd2  14388  cats1fv  14963  ege2le3  16209  cos2bnd  16309  3dvdsdec  16455  n2dvdsm1  16492  sumeven  16510  divalglem2  16518  pockthi  17032  dec2dvds  17188  prmlem1  17232  prmlem2  17245  1259prm  17261  2503prm  17265  4001prm  17270  vitalilem5  25880  dveflem  26246  tangtx  26783  sinq12ge0  26786  logi  26864  cxpge0  26960  asin1  27171  birthday  27231  lgamgulmlem4  27308  ppiub  27480  bposlem7  27566  lgsdir2lem2  27602  pthdlem2  30273  ex-fl  30967  ex-ind-dvds  30981  siilem2  31373  normlem6  31636  normlem7  31637  cm2mi  32147  pjnormi  32242  unierri  32625  dp2lt10  33369  dpgti  33391  pfx1s2  33425  cyc2fv2  33602  cyc3fv3  33619  hgt750lemd  35197  hgt750lem  35200  hgt750lem2  35201  hgt750leme  35207  cnndvlem1  37319  taupi  38158  poimirlem25  38477  poimirlem26  38478  poimirlem27  38479  poimirlem28  38480  ftc1anclem5  38529  fdc  38593  lcmineqlem23  43015  3lexlogpow2ineq2  43023  pellfundgt1  43822  jm2.27dlem2  43949  stoweidlem13  46939  sqwvfoura  47154  sqwvfourb  47155  fourierswlem  47156  goldrapos  47846  goldratval  47852  sinnpoly  47857  m1modnep2mod  48344  41prothprm  48620  nprmdvdsfacm1lem4  48624  tgblthelfgott  48829  tgoldbachlt  48830  nnlog2ge0lt1  49594  1aryenefmnd  49674  ackval42  49724