Theorem eqbrtrri 5127

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  3brtr3i  5133  expnass  14359  faclbnd4lem1  14444  sqrt2gt1lt2  15450  cos1bnd  16364  cos2bnd  16365  prdsvalstr  17632  chnub  18805  ovolre  25855  pigt3  26855  pige3ALT  26857  atan1  27265  log2ublem1  27283  sqrtlim  27309  bposlem8  27627  chebbnd1  27808  norm-ii-i  31748  nmopadji  32701  unierri  32715  ballotlem2  35171  hgt750lemd  35327  hgt750lem  35330  stoweidlem26  47144  wallispilem5  47187