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

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
StepHypRef Expression
1 eqbrtrr.1 . . 3 𝐴 = 𝐵
21eqcomi 2779 . 2 𝐵 = 𝐴
3 eqbrtrr.2 . 2 𝐴𝑅𝐶
42, 3eqbrtri 4805 1 𝐵𝑅𝐶
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator