Theorem eqbrtrri 5133

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

Syntax hints:   = wceq 1540   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  3brtr3i  5139  expnass  14180  faclbnd4lem1  14265  sqrt2gt1lt2  15247  cos1bnd  16162  cos2bnd  16163  prdsvalstr  17422  ovolre  25433  pigt3  26434  pige3ALT  26436  atan1  26845  log2ublem1  26863  sqrtlim  26890  bposlem8  27209  chebbnd1  27390  norm-ii-i  31073  nmopadji  32026  unierri  32040  chnub  32945  ballotlem2  34487  hgt750lemd  34646  hgt750lem  34649  stoweidlem26  46031  wallispilem5  46074