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

Theorem breqtrri 5133
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 2746 . 2 𝐵 = 𝐶
41, 3breqtri 5131 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  3brtr4i  5136  ensn1  8962  ensn1OLD  8963  1sdom2ALT  9186  dju1p1e2ALT  10111  infmap2  10155  0lt1sr  11032  0le2  12256  2pos  12257  3pos  12259  4pos  12261  5pos  12263  6pos  12264  7pos  12265  8pos  12266  9pos  12267  1lt2  12325  2lt3  12326  3lt4  12328  4lt5  12331  5lt6  12335  6lt7  12340  7lt8  12346  8lt9  12353  nn0le2xi  12468  numltc  12645  declti  12657  xlemul1a  13208  sqge0i  14093  faclbnd2  14192  cats1fv  14749  ege2le3  15973  cos2bnd  16071  3dvdsdec  16215  n2dvdsm1  16252  sumeven  16270  divalglem2  16278  pockthi  16780  dec2dvds  16936  prmlem1  16981  prmlem2  16993  1259prm  17009  2503prm  17013  4001prm  17018  2strstr1OLD  17110  vitalilem5  24979  dveflem  25346  tangtx  25865  sinq12ge0  25868  cxpge0  26041  asin1  26247  birthday  26307  lgamgulmlem4  26384  ppiub  26555  bposlem7  26641  lgsdir2lem2  26677  pthdlem2  28719  ex-fl  29394  ex-ind-dvds  29408  siilem2  29797  normlem6  30060  normlem7  30061  cm2mi  30571  pjnormi  30666  unierri  31049  dp2lt10  31743  dpgti  31765  pfx1s2  31798  cyc2fv2  31974  cyc3fv3  31991  hgt750lemd  33264  hgt750lem  33267  hgt750lem2  33268  hgt750leme  33274  logi  34310  cnndvlem1  35003  taupi  35797  poimirlem25  36106  poimirlem26  36107  poimirlem27  36108  poimirlem28  36109  ftc1anclem5  36158  fdc  36207  lcmineqlem23  40511  3lexlogpow2ineq2  40519  pellfundgt1  41209  jm2.27dlem2  41337  stoweidlem13  44261  sqwvfoura  44476  sqwvfourb  44477  fourierswlem  44478  tworepnotupword  45132  41prothprm  45818  tgblthelfgott  46014  tgoldbachlt  46015  nnlog2ge0lt1  46659  1aryenefmnd  46739  ackval42  46789
  Copyright terms: Public domain W3C validator