Theorem eqbrtrri 5172

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 2742	. 2 ⊢ 𝐵 = 𝐴
3		eqbrtrr.2	. 2 ⊢ 𝐴𝑅𝐶
4	2, 3	eqbrtri 5170	1 ⊢ 𝐵𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5149

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  3brtr3i  5178  expnass  14172  faclbnd4lem1  14253  sqrt2gt1lt2  15221  cos1bnd  16130  cos2bnd  16131  2strstr1OLD  17170  prdsvalstr  17398  ovolre  25042  pigt3  26027  pige3ALT  26029  atan1  26433  log2ublem1  26451  sqrtlim  26477  bposlem8  26794  chebbnd1  26975  norm-ii-i  30390  nmopadji  31343  unierri  31357  ballotlem2  33487  hgt750lemd  33660  hgt750lem  33663  stoweidlem26  44742  wallispilem5  44785