Theorem breqtrri 5131

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  3brtr4i  5134  ensn1  9048  1sdom2ALT  9240  dju1p1e2ALT  10253  infmap2  10295  0lt1sr  11180  0le2OLD  12446  2posOLD  12448  1lt2  12515  2lt3  12516  3lt4  12519  4lt5  12522  5lt6  12526  6lt7  12531  7lt8  12537  8lt9  12544  numltc  12845  declti  12857  xlemul1a  13418  sqge0i  14331  faclbnd2  14435  cats1fv  15010  ege2le3  16256  cos2bnd  16356  3dvdsdec  16502  n2dvdsm1  16539  sumeven  16557  divalglem2  16565  pockthi  17085  dec2dvds  17241  prmlem1  17285  prmlem2  17298  1259prm  17314  2503prm  17318  4001prm  17323  vitalilem5  25933  dveflem  26299  tangtx  26834  sinq12ge0  26837  logi  26915  cxpge0  27011  asin1  27222  birthday  27282  lgamgulmlem4  27359  ppiub  27531  bposlem7  27617  lgsdir2lem2  27653  pthdlem2  30354  ex-fl  31048  ex-ind-dvds  31062  siilem2  31454  normlem6  31717  normlem7  31718  cm2mi  32228  pjnormi  32323  unierri  32706  dp2lt10  33450  dpgti  33472  pfx1s2  33506  cyc2fv2  33683  cyc3fv3  33700  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  cnndvlem1  37403  taupi  38245  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  ftc1anclem5  38616  fdc  38680  lcmineqlem23  43102  3lexlogpow2ineq2  43110  pellfundgt1  43890  jm2.27dlem2  44017  stoweidlem13  47023  sqwvfoura  47238  sqwvfourb  47239  fourierswlem  47240  goldrapos  47930  goldratval  47936  sinnpoly  47941  m1modnep2mod  48428  41prothprm  48704  nprmdvdsfacm1lem4  48708  tgblthelfgott  48913  tgoldbachlt  48914  nnlog2ge0lt1  49678  1aryenefmnd  49758  ackval42  49808