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

Theorem breqtrri 4472
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
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 2480 . 2  |-  B  =  C
41, 3breqtri 4470 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  3brtr4i  4475  ensn1  7579  1sdom2  7718  pm110.643ALT  8557  infmap2  8597  0lt1sr  9471  0le2  10625  2pos  10626  3pos  10628  4pos  10630  5pos  10632  6pos  10633  7pos  10634  8pos  10635  9pos  10636  10pos  10637  1lt2  10701  2lt3  10702  3lt4  10704  4lt5  10707  5lt6  10711  6lt7  10716  7lt8  10722  8lt9  10729  9lt10  10737  nn0le2xi  10846  numltc  10995  declti  11000  xlemul1a  11479  sqge0i  12222  faclbnd2  12336  cats1fv  12786  ege2le3  13686  cos2bnd  13783  divalglem2  13911  pockthi  14283  dec2dvds  14407  prmlem1  14450  prmlem2  14462  1259prm  14475  2503prm  14479  4001prm  14484  vitalilem5  21772  dveflem  22131  tangtx  22647  sinq12ge0  22650  cxpge0  22808  asin1  22969  birthday  23028  ppiub  23223  bposlem4  23306  bposlem5  23307  bposlem7  23309  lgsdir2lem2  23343  ex-fl  24861  siilem2  25459  normlem6  25724  normlem7  25725  cm2mi  26236  pjnormi  26331  unierri  26715  lgamgulmlem4  28230  ftc1anclem5  29687  fdc  29857  pellfundgt1  30439  jm2.27dlem2  30572  stoweidlem13  31329  taupi  36778
  Copyright terms: Public domain W3C validator