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

Theorem eqbrtrri 4415
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
eqbrtrr.1  |-  A  =  B
eqbrtrr.2  |-  A R C
Assertion
Ref Expression
eqbrtrri  |-  B R C

Proof of Theorem eqbrtrri
StepHypRef Expression
1 eqbrtrr.1 . . 3  |-  A  =  B
21eqcomi 2415 . 2  |-  B  =  A
3 eqbrtrr.2 . 2  |-  A R C
42, 3eqbrtri 4413 1  |-  B R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405   class class class wbr 4394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395
This theorem is referenced by:  3brtr3i  4421  expnass  12228  faclbnd4lem1  12325  sqrt2gt1lt2  13164  cos1bnd  14023  cos2bnd  14024  prdsvalstr  14959  ovolre  22120  pige3  23094  atan1  23476  log2ublem1  23494  sqrtlim  23520  bposlem8  23839  chebbnd1  23930  konigsberg  25285  norm-ii-i  26348  nmopadji  27302  unierri  27316  ballotlem2  28813  stoweidlem26  37158  wallispilem5  37201
  Copyright terms: Public domain W3C validator