Theorem breqtrri 5122

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

Syntax hints:   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  3brtr4i  5125  ensn1  8953  1sdom2ALT  9143  dju1p1e2ALT  10076  infmap2  10118  0lt1sr  10996  0le2  12237  2pos  12238  3pos  12240  4pos  12242  5pos  12244  6pos  12245  7pos  12246  8pos  12247  9pos  12248  1lt2  12301  2lt3  12302  3lt4  12304  4lt5  12307  5lt6  12311  6lt7  12316  7lt8  12322  8lt9  12329  numltc  12624  declti  12636  xlemul1a  13197  sqge0i  14105  faclbnd2  14208  cats1fv  14776  ege2le3  16007  cos2bnd  16107  3dvdsdec  16253  n2dvdsm1  16290  sumeven  16308  divalglem2  16316  pockthi  16829  dec2dvds  16985  prmlem1  17029  prmlem2  17041  1259prm  17057  2503prm  17061  4001prm  17066  vitalilem5  25550  dveflem  25920  tangtx  26451  sinq12ge0  26454  logi  26533  cxpge0  26629  asin1  26841  birthday  26901  lgamgulmlem4  26979  ppiub  27152  bposlem7  27238  lgsdir2lem2  27274  pthdlem2  29757  ex-fl  30438  ex-ind-dvds  30452  siilem2  30843  normlem6  31106  normlem7  31107  cm2mi  31617  pjnormi  31712  unierri  32095  dp2lt10  32875  dpgti  32897  pfx1s2  32931  cyc2fv2  33102  cyc3fv3  33119  hgt750lemd  34672  hgt750lem  34675  hgt750lem2  34676  hgt750leme  34682  cnndvlem1  36592  taupi  37378  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem28  37698  ftc1anclem5  37747  fdc  37795  lcmineqlem23  42154  3lexlogpow2ineq2  42162  pellfundgt1  42990  jm2.27dlem2  43117  stoweidlem13  46125  sqwvfoura  46340  sqwvfourb  46341  fourierswlem  46342  m1modnep2mod  47466  41prothprm  47733  tgblthelfgott  47929  tgoldbachlt  47930  nnlog2ge0lt1  48681  1aryenefmnd  48761  ackval42  48811