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

Theorem breqtrri 4329
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 2447 . 2  |-  B  =  C
41, 3breqtri 4327 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   class class class wbr 4304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305
This theorem is referenced by:  3brtr4i  4332  ensn1  7385  1sdom2  7523  pm110.643ALT  8359  infmap2  8399  0lt1sr  9274  0le2  10424  2pos  10425  3pos  10427  4pos  10429  5pos  10431  6pos  10432  7pos  10433  8pos  10434  9pos  10435  10pos  10436  1lt2  10500  2lt3  10501  3lt4  10503  4lt5  10506  5lt6  10510  6lt7  10515  7lt8  10521  8lt9  10528  9lt10  10536  nn0le2xi  10643  numltc  10787  declti  10792  xlemul1a  11263  sqge0i  11965  faclbnd2  12079  cats1fv  12498  ege2le3  13387  cos2bnd  13484  divalglem2  13611  pockthi  13980  dec2dvds  14104  prmlem1  14147  prmlem2  14159  1259prm  14172  2503prm  14176  4001prm  14181  vitalilem5  21104  dveflem  21463  tangtx  21979  sinq12ge0  21982  cxpge0  22140  asin1  22301  birthday  22360  ppiub  22555  bposlem4  22638  bposlem5  22639  bposlem7  22641  lgsdir2lem2  22675  ex-fl  23666  siilem2  24264  normlem6  24529  normlem7  24530  cm2mi  25041  pjnormi  25136  unierri  25520  lgamgulmlem4  27030  ftc1anclem5  28483  fdc  28653  pellfundgt1  29236  jm2.27dlem2  29371  stoweidlem13  29820  taupi  35629
  Copyright terms: Public domain W3C validator