Theorem breqtrri 4680

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

Syntax hints:   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  3brtr4i  4683  ensn1  8020  1sdom2  8159  pm110.643ALT  9000  infmap2  9040  0lt1sr  9916  0le2  11111  2pos  11112  3pos  11114  4pos  11116  5pos  11118  6pos  11119  7pos  11120  8pos  11121  9pos  11122  10posOLD  11123  1lt2  11194  2lt3  11195  3lt4  11197  4lt5  11200  5lt6  11204  6lt7  11209  7lt8  11215  8lt9  11222  9lt10OLD  11230  nn0le2xi  11347  numltc  11528  declti  11546  decltiOLD  11548  xlemul1a  12118  sqge0i  12951  faclbnd2  13078  cats1fv  13604  ege2le3  14820  cos2bnd  14918  3dvdsdec  15054  3dvdsdecOLD  15055  n2dvdsm1  15105  n2dvds3  15107  sumeven  15110  divalglem2  15118  pockthi  15611  dec2dvds  15767  prmlem1  15814  prmlem2  15827  1259prm  15843  2503prm  15847  4001prm  15852  2strstr1  15986  vitalilem5  23381  dveflem  23742  tangtx  24257  sinq12ge0  24260  cxpge0  24429  asin1  24621  birthday  24681  lgamgulmlem4  24758  ppiub  24929  bposlem7  25015  lgsdir2lem2  25051  pthdlem2  26664  ex-fl  27304  ex-ind-dvds  27318  siilem2  27707  normlem6  27972  normlem7  27973  cm2mi  28485  pjnormi  28580  unierri  28963  dp2lt10  29591  dpgti  29614  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  logi  31620  cnndvlem1  32528  taupi  33169  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  ftc1anclem5  33489  fdc  33541  pellfundgt1  37447  jm2.27dlem2  37577  stoweidlem13  40230  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  41prothprm  41536  tgblthelfgott  41703  tgoldbachlt  41704  tgblthelfgottOLD  41709  tgoldbachltOLD  41710  nnlog2ge0lt1  42360