Theorem eqbrtrri 5128

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  3brtr3i  5134  expnass  14272  faclbnd4lem1  14357  sqrt2gt1lt2  15361  cos1bnd  16275  cos2bnd  16276  prdsvalstr  17537  chnub  18710  ovolre  25753  pigt3  26755  pige3ALT  26757  atan1  27165  log2ublem1  27183  sqrtlim  27209  bposlem8  27527  chebbnd1  27708  norm-ii-i  31618  nmopadji  32571  unierri  32585  ballotlem2  35000  hgt750lemd  35156  hgt750lem  35159  stoweidlem26  46854  wallispilem5  46897