Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqbrtrri Structured version   Visualization version   GIF version

Theorem eqbrtrri 5053
 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
StepHypRef Expression
1 eqbrtrr.1 . . 3 𝐴 = 𝐵
21eqcomi 2807 . 2 𝐵 = 𝐴
3 eqbrtrr.2 . 2 𝐴𝑅𝐶
42, 3eqbrtri 5051 1 𝐵𝑅𝐶
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   class class class wbr 5030 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031 This theorem is referenced by:  3brtr3i  5059  expnass  13568  faclbnd4lem1  13651  sqrt2gt1lt2  14628  cos1bnd  15534  cos2bnd  15535  2strstr1  16599  prdsvalstr  16720  ovolre  24136  pigt3  25117  pige3ALT  25119  atan1  25521  log2ublem1  25539  sqrtlim  25565  bposlem8  25882  chebbnd1  26063  norm-ii-i  28927  nmopadji  29880  unierri  29894  ballotlem2  31868  hgt750lemd  32041  hgt750lem  32044  3lexlogpow5ineq1  39357  stoweidlem26  42683  wallispilem5  42726
 Copyright terms: Public domain W3C validator