Theorem breqtrri 5174

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

Syntax hints:   = wceq 1539   class class class wbr 5147

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  3brtr4i  5177  ensn1  9019  ensn1OLD  9020  1sdom2ALT  9243  dju1p1e2ALT  10171  infmap2  10215  0lt1sr  11092  0le2  12318  2pos  12319  3pos  12321  4pos  12323  5pos  12325  6pos  12326  7pos  12327  8pos  12328  9pos  12329  1lt2  12387  2lt3  12388  3lt4  12390  4lt5  12393  5lt6  12397  6lt7  12402  7lt8  12408  8lt9  12415  nn0le2xi  12530  numltc  12707  declti  12719  xlemul1a  13271  sqge0i  14156  faclbnd2  14255  cats1fv  14814  ege2le3  16037  cos2bnd  16135  3dvdsdec  16279  n2dvdsm1  16316  sumeven  16334  divalglem2  16342  pockthi  16844  dec2dvds  17000  prmlem1  17045  prmlem2  17057  1259prm  17073  2503prm  17077  4001prm  17082  2strstr1OLD  17174  vitalilem5  25361  dveflem  25731  tangtx  26251  sinq12ge0  26254  cxpge0  26427  asin1  26635  birthday  26695  lgamgulmlem4  26772  ppiub  26943  bposlem7  27029  lgsdir2lem2  27065  n0scut  27943  pthdlem2  29292  ex-fl  29967  ex-ind-dvds  29981  siilem2  30372  normlem6  30635  normlem7  30636  cm2mi  31146  pjnormi  31241  unierri  31624  dp2lt10  32317  dpgti  32339  pfx1s2  32372  cyc2fv2  32551  cyc3fv3  32568  hgt750lemd  33958  hgt750lem  33961  hgt750lem2  33962  hgt750leme  33968  logi  35008  cnndvlem1  35716  taupi  36507  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  ftc1anclem5  36868  fdc  36916  lcmineqlem23  41222  3lexlogpow2ineq2  41230  pellfundgt1  41923  jm2.27dlem2  42051  stoweidlem13  45027  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  tworepnotupword  45898  41prothprm  46585  tgblthelfgott  46781  tgoldbachlt  46782  nnlog2ge0lt1  47339  1aryenefmnd  47419  ackval42  47469