Theorem eqbrtrri 4807

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

Syntax hints:   = wceq 1630   class class class wbr 4784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785

This theorem is referenced by:  3brtr3i  4813  expnass  13176  faclbnd4lem1  13283  sqrt2gt1lt2  14222  cos1bnd  15122  cos2bnd  15123  2strstr1  16193  prdsvalstr  16320  ovolre  23512  pige3  24489  atan1  24875  log2ublem1  24893  sqrtlim  24919  bposlem8  25236  chebbnd1  25381  norm-ii-i  28328  nmopadji  29283  unierri  29297  ballotlem2  30884  hgt750lemd  31060  hgt750lem  31063  pigt3  33728  stoweidlem26  40754  wallispilem5  40797