Theorem eqbrtrri 5136

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  3brtr3i  5142  expnass  14262  faclbnd4lem1  14347  sqrt2gt1lt2  15349  cos1bnd  16265  cos2bnd  16266  prdsvalstr  17527  chnub  18700  ovolre  25735  pigt3  26734  pige3ALT  26736  atan1  27144  log2ublem1  27162  sqrtlim  27188  bposlem8  27506  chebbnd1  27687  norm-ii-i  31560  nmopadji  32513  unierri  32527  ballotlem2  34944  hgt750lemd  35100  hgt750lem  35103  stoweidlem26  46798  wallispilem5  46841