Theorem eqbrtrri 5170

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

Syntax hints:   = wceq 1539   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  3brtr3i  5176  expnass  14176  faclbnd4lem1  14257  sqrt2gt1lt2  15225  cos1bnd  16134  cos2bnd  16135  2strstr1OLD  17174  prdsvalstr  17402  ovolre  25274  pigt3  26263  pige3ALT  26265  atan1  26669  log2ublem1  26687  sqrtlim  26713  bposlem8  27030  chebbnd1  27211  norm-ii-i  30657  nmopadji  31610  unierri  31624  ballotlem2  33785  hgt750lemd  33958  hgt750lem  33961  stoweidlem26  45040  wallispilem5  45083