Theorem eqbrtrri 5097

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 5095	1 ⊢ 𝐵𝑅𝐶

Syntax hints:   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  3brtr3i  5103  expnass  13924  faclbnd4lem1  14007  sqrt2gt1lt2  14986  cos1bnd  15896  cos2bnd  15897  2strstr1OLD  16938  prdsvalstr  17163  ovolre  24689  pigt3  25674  pige3ALT  25676  atan1  26078  log2ublem1  26096  sqrtlim  26122  bposlem8  26439  chebbnd1  26620  norm-ii-i  29499  nmopadji  30452  unierri  30466  ballotlem2  32455  hgt750lemd  32628  hgt750lem  32631  stoweidlem26  43567  wallispilem5  43610