Theorem breqtrri 5129

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

Syntax hints:   = wceq 1540   class class class wbr 5102

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  3brtr4i  5132  ensn1  8969  1sdom2ALT  9165  dju1p1e2ALT  10104  infmap2  10146  0lt1sr  11024  0le2  12264  2pos  12265  3pos  12267  4pos  12269  5pos  12271  6pos  12272  7pos  12273  8pos  12274  9pos  12275  1lt2  12328  2lt3  12329  3lt4  12331  4lt5  12334  5lt6  12338  6lt7  12343  7lt8  12349  8lt9  12356  numltc  12651  declti  12663  xlemul1a  13224  sqge0i  14129  faclbnd2  14232  cats1fv  14801  ege2le3  16032  cos2bnd  16132  3dvdsdec  16278  n2dvdsm1  16315  sumeven  16333  divalglem2  16341  pockthi  16854  dec2dvds  17010  prmlem1  17054  prmlem2  17066  1259prm  17082  2503prm  17086  4001prm  17091  vitalilem5  25546  dveflem  25916  tangtx  26447  sinq12ge0  26450  logi  26529  cxpge0  26625  asin1  26837  birthday  26897  lgamgulmlem4  26975  ppiub  27148  bposlem7  27234  lgsdir2lem2  27270  pthdlem2  29748  ex-fl  30426  ex-ind-dvds  30440  siilem2  30831  normlem6  31094  normlem7  31095  cm2mi  31605  pjnormi  31700  unierri  32083  dp2lt10  32854  dpgti  32876  pfx1s2  32910  cyc2fv2  33094  cyc3fv3  33111  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  cnndvlem1  36518  taupi  37304  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  ftc1anclem5  37684  fdc  37732  lcmineqlem23  42032  3lexlogpow2ineq2  42040  pellfundgt1  42864  jm2.27dlem2  42992  stoweidlem13  46004  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  tworepnotupword  46877  m1modnep2mod  47346  41prothprm  47613  tgblthelfgott  47809  tgoldbachlt  47810  nnlog2ge0lt1  48548  1aryenefmnd  48628  ackval42  48678