Theorem breqtrri 5181

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

Syntax hints:   = wceq 1534   class class class wbr 5154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-rab 3429  df-v 3474  df-dif 3961  df-un 3963  df-ss 3975  df-nul 4334  df-if 4535  df-sn 4635  df-pr 4637  df-op 4641  df-br 5155

This theorem is referenced by:  3brtr4i  5184  ensn1  9057  ensn1OLD  9058  1sdom2ALT  9279  dju1p1e2ALT  10219  infmap2  10261  0lt1sr  11139  0le2  12370  2pos  12371  3pos  12373  4pos  12375  5pos  12377  6pos  12378  7pos  12379  8pos  12380  9pos  12381  1lt2  12439  2lt3  12440  3lt4  12442  4lt5  12445  5lt6  12449  6lt7  12454  7lt8  12460  8lt9  12467  nn0le2xi  12582  numltc  12759  declti  12771  xlemul1a  13325  sqge0i  14211  faclbnd2  14314  cats1fv  14881  ege2le3  16105  cos2bnd  16203  3dvdsdec  16347  n2dvdsm1  16384  sumeven  16402  divalglem2  16410  pockthi  16922  dec2dvds  17078  prmlem1  17123  prmlem2  17135  1259prm  17151  2503prm  17155  4001prm  17160  2strstr1OLD  17252  vitalilem5  25632  dveflem  26002  tangtx  26530  sinq12ge0  26533  logi  26611  cxpge0  26707  asin1  26919  birthday  26979  lgamgulmlem4  27057  ppiub  27230  bposlem7  27316  lgsdir2lem2  27352  n0scut  28303  pthdlem2  29702  ex-fl  30377  ex-ind-dvds  30391  siilem2  30782  normlem6  31045  normlem7  31046  cm2mi  31556  pjnormi  31651  unierri  32034  dp2lt10  32748  dpgti  32770  pfx1s2  32805  cyc2fv2  33015  cyc3fv3  33032  hgt750lemd  34525  hgt750lem  34528  hgt750lem2  34529  hgt750leme  34535  cnndvlem1  36281  taupi  37070  poimirlem25  37386  poimirlem26  37387  poimirlem27  37388  poimirlem28  37389  ftc1anclem5  37438  fdc  37486  lcmineqlem23  41790  3lexlogpow2ineq2  41798  pellfundgt1  42607  jm2.27dlem2  42735  stoweidlem13  45700  sqwvfoura  45915  sqwvfourb  45916  fourierswlem  45917  tworepnotupword  46571  41prothprm  47257  tgblthelfgott  47453  tgoldbachlt  47454  nnlog2ge0lt1  48031  1aryenefmnd  48111  ackval42  48161