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

Theorem breqtrri 4048
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
breqtrr.1  |-  A R B
breqtrr.2  |-  C  =  B
Assertion
Ref Expression
breqtrri  |-  A R C

Proof of Theorem breqtrri
StepHypRef Expression
1 breqtrr.1 . 2  |-  A R B
2 breqtrr.2 . . 3  |-  C  =  B
32eqcomi 2287 . 2  |-  B  =  C
41, 3breqtri 4046 1  |-  A R C
Colors of variables: wff set class
Syntax hints:    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  3brtr4i  4051  ensn1  6925  1sdom2  7061  pm110.643ALT  7804  infmap2  7844  0lt1sr  8717  2pos  9828  3pos  9830  4pos  9832  5pos  9833  6pos  9834  7pos  9835  8pos  9836  9pos  9837  10pos  9838  1lt2  9886  2lt3  9887  3lt4  9889  4lt5  9892  5lt6  9896  6lt7  9901  7lt8  9907  8lt9  9914  9lt10  9922  nn0le2xi  10015  numltc  10144  declti  10149  xlemul1a  10608  sqge0i  11191  faclbnd2  11304  cats1fv  11509  ege2le3  12371  cos2bnd  12468  divalglem2  12594  pockthi  12954  dec2dvds  13078  prmlem1  13109  prmlem2  13121  1259prm  13134  2503prm  13138  4001prm  13143  vitalilem5  18967  dveflem  19326  tangtx  19873  sinq12ge0  19876  cxpge0  20030  asin1  20190  birthday  20249  ppiub  20443  bposlem4  20526  bposlem5  20527  bposlem7  20529  lgsdir2lem2  20563  ex-fl  20834  siilem2  21430  normlem6  21694  normlem7  21695  cm2mi  22205  pjnormi  22300  unierri  22684  fdc  26455  pellfundgt1  26968  jm2.27dlem2  27103  stoweidlem13  27762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator