Theorem eqbrtrri 5095

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

Syntax hints:   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  3brtr3i  5101  expnass  14161  faclbnd4lem1  14246  sqrt2gt1lt2  15227  cos1bnd  16145  cos2bnd  16146  prdsvalstr  17406  chnub  18579  ovolre  25510  pigt3  26500  pige3ALT  26502  atan1  26910  log2ublem1  26928  sqrtlim  26954  bposlem8  27272  chebbnd1  27453  norm-ii-i  31226  nmopadji  32179  unierri  32193  ballotlem2  34673  hgt750lemd  34832  hgt750lem  34835  stoweidlem26  46469  wallispilem5  46512