Theorem breqtrri 4610

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

Syntax hints:   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  3brtr4i  4613  ensn1  7906  1sdom2  8044  pm110.643ALT  8883  infmap2  8923  0lt1sr  9795  0le2  10988  2pos  10989  3pos  10991  4pos  10993  5pos  10995  6pos  10996  7pos  10997  8pos  10998  9pos  10999  10posOLD  11000  1lt2  11071  2lt3  11072  3lt4  11074  4lt5  11077  5lt6  11081  6lt7  11086  7lt8  11092  8lt9  11099  9lt10OLD  11107  nn0le2xi  11224  numltc  11404  declti  11422  decltiOLD  11424  xlemul1a  11990  sqge0i  12813  faclbnd2  12940  cats1fv  13455  ege2le3  14659  cos2bnd  14757  3dvdsdec  14892  3dvdsdecOLD  14893  n2dvdsm1  14943  n2dvds3  14945  sumeven  14948  divalglem2  14956  pockthi  15449  dec2dvds  15605  prmlem1  15652  prmlem2  15665  1259prm  15681  2503prm  15685  4001prm  15690  2strstr1  15812  vitalilem5  23187  dveflem  23546  tangtx  24061  sinq12ge0  24064  cxpge0  24229  asin1  24421  birthday  24481  lgamgulmlem4  24558  ppiub  24729  bposlem7  24815  lgsdir2lem2  24851  ex-fl  26696  ex-ind-dvds  26710  siilem2  27091  normlem6  27356  normlem7  27357  cm2mi  27869  pjnormi  27964  unierri  28347  logi  30873  cnndvlem1  31698  taupi  32346  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  ftc1anclem5  32659  fdc  32711  pellfundgt1  36465  jm2.27dlem2  36595  stoweidlem13  38906  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  41prothprm  40074  tgblthelfgott  40229  tgoldbachlt  40230  tgblthelfgottOLD  40236  tgoldbachltOLD  40237  pthdlem2  40974  nnlog2ge0lt1  42158