Theorem eqbrtrri 5093

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtrr.1	⊢ 𝐴 = 𝐵
eqbrtrr.2	⊢ 𝐴𝑅𝐶

Assertion

Ref	Expression
eqbrtrri	⊢ 𝐵𝑅𝐶

Proof of Theorem eqbrtrri

Step	Hyp	Ref	Expression
1		eqbrtrr.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2747	. 2 ⊢ 𝐵 = 𝐴
3		eqbrtrr.2	. 2 ⊢ 𝐴𝑅𝐶
4	2, 3	eqbrtri 5091	1 ⊢ 𝐵𝑅𝐶

Syntax hints:   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  3brtr3i  5099  expnass  13852  faclbnd4lem1  13935  sqrt2gt1lt2  14914  cos1bnd  15824  cos2bnd  15825  2strstr1OLD  16864  prdsvalstr  17080  ovolre  24594  pigt3  25579  pige3ALT  25581  atan1  25983  log2ublem1  26001  sqrtlim  26027  bposlem8  26344  chebbnd1  26525  norm-ii-i  29400  nmopadji  30353  unierri  30367  ballotlem2  32355  hgt750lemd  32528  hgt750lem  32531  stoweidlem26  43457  wallispilem5  43500