Theorem eqbrtrri 5127

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

Syntax hints:   = wceq 1541   class class class wbr 5104

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105

This theorem is referenced by:  3brtr3i  5133  expnass  14109  faclbnd4lem1  14190  sqrt2gt1lt2  15156  cos1bnd  16066  cos2bnd  16067  2strstr1OLD  17106  prdsvalstr  17331  ovolre  24885  pigt3  25870  pige3ALT  25872  atan1  26274  log2ublem1  26292  sqrtlim  26318  bposlem8  26635  chebbnd1  26816  norm-ii-i  29977  nmopadji  30930  unierri  30944  ballotlem2  32979  hgt750lemd  33152  hgt750lem  33155  stoweidlem26  44237  wallispilem5  44280