Theorem breqtrri 5137

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

Syntax hints:   = wceq 1540   class class class wbr 5110

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  3brtr4i  5140  ensn1  8995  1sdom2ALT  9195  dju1p1e2ALT  10135  infmap2  10177  0lt1sr  11055  0le2  12295  2pos  12296  3pos  12298  4pos  12300  5pos  12302  6pos  12303  7pos  12304  8pos  12305  9pos  12306  1lt2  12359  2lt3  12360  3lt4  12362  4lt5  12365  5lt6  12369  6lt7  12374  7lt8  12380  8lt9  12387  numltc  12682  declti  12694  xlemul1a  13255  sqge0i  14160  faclbnd2  14263  cats1fv  14832  ege2le3  16063  cos2bnd  16163  3dvdsdec  16309  n2dvdsm1  16346  sumeven  16364  divalglem2  16372  pockthi  16885  dec2dvds  17041  prmlem1  17085  prmlem2  17097  1259prm  17113  2503prm  17117  4001prm  17122  vitalilem5  25520  dveflem  25890  tangtx  26421  sinq12ge0  26424  logi  26503  cxpge0  26599  asin1  26811  birthday  26871  lgamgulmlem4  26949  ppiub  27122  bposlem7  27208  lgsdir2lem2  27244  pthdlem2  29705  ex-fl  30383  ex-ind-dvds  30397  siilem2  30788  normlem6  31051  normlem7  31052  cm2mi  31562  pjnormi  31657  unierri  32040  dp2lt10  32811  dpgti  32833  pfx1s2  32867  cyc2fv2  33086  cyc3fv3  33103  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  cnndvlem1  36532  taupi  37318  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  ftc1anclem5  37698  fdc  37746  lcmineqlem23  42046  3lexlogpow2ineq2  42054  pellfundgt1  42878  jm2.27dlem2  43006  stoweidlem13  46018  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  tworepnotupword  46891  m1modnep2mod  47357  41prothprm  47624  tgblthelfgott  47820  tgoldbachlt  47821  nnlog2ge0lt1  48559  1aryenefmnd  48639  ackval42  48689