Theorem eqbrtrri 5118

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

Syntax hints:   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  3brtr3i  5124  expnass  14122  faclbnd4lem1  14207  sqrt2gt1lt2  15188  cos1bnd  16103  cos2bnd  16104  prdsvalstr  17363  chnub  18536  ovolre  25473  pigt3  26474  pige3ALT  26476  atan1  26885  log2ublem1  26903  sqrtlim  26930  bposlem8  27249  chebbnd1  27430  norm-ii-i  31138  nmopadji  32091  unierri  32105  ballotlem2  34574  hgt750lemd  34733  hgt750lem  34736  stoweidlem26  46186  wallispilem5  46229