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

Theorem breqtrri 5057
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
breqtrr.1 𝐴𝑅𝐵
breqtrr.2 𝐶 = 𝐵
Assertion
Ref Expression
breqtrri 𝐴𝑅𝐶

Proof of Theorem breqtrri
StepHypRef Expression
1 breqtrr.1 . 2 𝐴𝑅𝐵
2 breqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2807 . 2 𝐵 = 𝐶
41, 3breqtri 5055 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538   class class class wbr 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031
This theorem is referenced by:  3brtr4i  5060  ensn1  8556  1sdom2  8701  dju1p1e2ALT  9585  infmap2  9629  0lt1sr  10506  0le2  11727  2pos  11728  3pos  11730  4pos  11732  5pos  11734  6pos  11735  7pos  11736  8pos  11737  9pos  11738  1lt2  11796  2lt3  11797  3lt4  11799  4lt5  11802  5lt6  11806  6lt7  11811  7lt8  11817  8lt9  11824  nn0le2xi  11939  numltc  12112  declti  12124  xlemul1a  12669  sqge0i  13547  faclbnd2  13647  cats1fv  14212  ege2le3  15435  cos2bnd  15533  3dvdsdec  15673  n2dvdsm1  15710  sumeven  15728  divalglem2  15736  pockthi  16233  dec2dvds  16389  prmlem1  16433  prmlem2  16445  1259prm  16461  2503prm  16465  4001prm  16470  2strstr1  16597  vitalilem5  24216  dveflem  24582  tangtx  25098  sinq12ge0  25101  cxpge0  25274  asin1  25480  birthday  25540  lgamgulmlem4  25617  ppiub  25788  bposlem7  25874  lgsdir2lem2  25910  pthdlem2  27557  ex-fl  28232  ex-ind-dvds  28246  siilem2  28635  normlem6  28898  normlem7  28899  cm2mi  29409  pjnormi  29504  unierri  29887  dp2lt10  30586  dpgti  30608  pfx1s2  30641  cyc2fv2  30814  cyc3fv3  30831  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  hgt750leme  32039  logi  33079  cnndvlem1  33989  taupi  34737  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  ftc1anclem5  35134  fdc  35183  lcmineqlem23  39339  pellfundgt1  39822  jm2.27dlem2  39949  stoweidlem13  42653  sqwvfoura  42868  sqwvfourb  42869  fourierswlem  42870  41prothprm  44135  tgblthelfgott  44331  tgoldbachlt  44332  nnlog2ge0lt1  44978  1aryenefmnd  45058  ackval42  45108
  Copyright terms: Public domain W3C validator