Theorem eqbrtrri 5134

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

Syntax hints:   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  3brtr3i  5140  expnass  14240  faclbnd4lem1  14325  sqrt2gt1lt2  15321  cos1bnd  16238  cos2bnd  16239  prdsvalstr  17500  chnub  18673  ovolre  25684  pigt3  26683  pige3ALT  26685  atan1  27093  log2ublem1  27111  sqrtlim  27137  bposlem8  27455  chebbnd1  27636  norm-ii-i  31489  nmopadji  32442  unierri  32456  ballotlem2  34879  hgt750lemd  35035  hgt750lem  35038  stoweidlem26  46740  wallispilem5  46783