Theorem breqtrri 5136

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  3brtr4i  5139  ensn1  9030  1sdom2ALT  9222  dju1p1e2ALT  10180  infmap2  10222  0lt1sr  11107  0le2OLD  12371  2posOLD  12373  1lt2  12440  2lt3  12441  3lt4  12444  4lt5  12447  5lt6  12451  6lt7  12456  7lt8  12462  8lt9  12469  numltc  12770  declti  12782  xlemul1a  13342  sqge0i  14254  faclbnd2  14357  cats1fv  14932  ege2le3  16180  cos2bnd  16280  3dvdsdec  16426  n2dvdsm1  16463  sumeven  16481  divalglem2  16489  pockthi  17003  dec2dvds  17159  prmlem1  17203  prmlem2  17216  1259prm  17232  2503prm  17236  4001prm  17241  vitalilem5  25841  dveflem  26208  tangtx  26740  sinq12ge0  26743  logi  26822  cxpge0  26918  asin1  27129  birthday  27189  lgamgulmlem4  27266  ppiub  27438  bposlem7  27524  lgsdir2lem2  27560  pthdlem2  30219  ex-fl  30913  ex-ind-dvds  30927  siilem2  31319  normlem6  31582  normlem7  31583  cm2mi  32093  pjnormi  32188  unierri  32571  dp2lt10  33316  dpgti  33338  pfx1s2  33372  cyc2fv2  33549  cyc3fv3  33566  hgt750lemd  35143  hgt750lem  35146  hgt750lem2  35147  hgt750leme  35153  cnndvlem1  37221  taupi  38062  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  ftc1anclem5  38433  fdc  38482  lcmineqlem23  42904  3lexlogpow2ineq2  42912  pellfundgt1  43711  jm2.27dlem2  43838  stoweidlem13  46828  sqwvfoura  47043  sqwvfourb  47044  fourierswlem  47045  goldrapos  47735  goldratval  47741  sinnpoly  47746  m1modnep2mod  48233  41prothprm  48509  nprmdvdsfacm1lem4  48513  tgblthelfgott  48718  tgoldbachlt  48719  nnlog2ge0lt1  49483  1aryenefmnd  49563  ackval42  49613