Theorem eqbrtrri 5138

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

Syntax hints:   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  3brtr3i  5144  expnass  14243  faclbnd4lem1  14328  sqrt2gt1lt2  15324  cos1bnd  16242  cos2bnd  16243  prdsvalstr  17504  chnub  18677  ovolre  25652  pigt3  26648  pige3ALT  26650  atan1  27058  log2ublem1  27076  sqrtlim  27102  bposlem8  27420  chebbnd1  27601  norm-ii-i  31429  nmopadji  32382  unierri  32396  ballotlem2  34823  hgt750lemd  34979  hgt750lem  34982  stoweidlem26  46631  wallispilem5  46674