Theorem breqtrri 5135

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  3brtr4i  5138  ensn1  9073  1sdom2ALT  9265  dju1p1e2ALT  10277  infmap2  10319  0lt1sr  11204  0le2OLD  12470  2posOLD  12472  1lt2  12539  2lt3  12540  3lt4  12543  4lt5  12546  5lt6  12550  6lt7  12555  7lt8  12561  8lt9  12568  numltc  12869  declti  12881  xlemul1a  13442  sqge0i  14355  faclbnd2  14459  cats1fv  15035  ege2le3  16282  cos2bnd  16382  3dvdsdec  16528  n2dvdsm1  16565  sumeven  16583  divalglem2  16591  pockthi  17111  dec2dvds  17267  prmlem1  17311  prmlem2  17324  1259prm  17340  2503prm  17344  4001prm  17349  vitalilem5  25960  dveflem  26326  tangtx  26861  sinq12ge0  26864  logi  26942  cxpge0  27038  asin1  27249  birthday  27309  lgamgulmlem4  27386  ppiub  27558  bposlem7  27644  lgsdir2lem2  27680  pthdlem2  30381  ex-fl  31075  ex-ind-dvds  31089  siilem2  31481  normlem6  31744  normlem7  31745  cm2mi  32255  pjnormi  32350  unierri  32733  dp2lt10  33517  dpgti  33539  pfx1s2  33573  cyc2fv2  33750  cyc3fv3  33767  hgt750lemd  35344  hgt750lem  35347  hgt750lem2  35348  hgt750leme  35354  cnndvlem1  37580  taupi  38435  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  ftc1anclem5  38806  fdc  38870  lcmineqlem23  43292  3lexlogpow2ineq2  43300  pellfundgt1  44081  jm2.27dlem2  44208  stoweidlem13  47226  sqwvfoura  47441  sqwvfourb  47442  fourierswlem  47443  goldrapos  48133  goldratval  48139  sinnpoly  48144  m1modnep2mod  48631  41prothprm  48907  nprmdvdsfacm1lem4  48911  tgblthelfgott  49116  tgoldbachlt  49117  nnlog2ge0lt1  49881  1aryenefmnd  49961  ackval42  50011