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

Theorem eqbrtrri 4827
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 2769 . 2 𝐵 = 𝐴
3 eqbrtrr.2 . 2 𝐴𝑅𝐶
42, 3eqbrtri 4825 1 𝐵𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805
This theorem is referenced by:  3brtr3i  4833  expnass  13164  faclbnd4lem1  13274  sqrt2gt1lt2  14214  cos1bnd  15116  cos2bnd  15117  2strstr1  16188  prdsvalstr  16315  ovolre  23493  pige3  24468  atan1  24854  log2ublem1  24872  sqrtlim  24898  bposlem8  25215  chebbnd1  25360  norm-ii-i  28303  nmopadji  29258  unierri  29272  ballotlem2  30859  hgt750lemd  31035  hgt750lem  31038  pigt3  33715  stoweidlem26  40746  wallispilem5  40789
  Copyright terms: Public domain W3C validator