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

Theorem breqtrri 4956
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 2788 . 2 𝐵 = 𝐶
41, 3breqtri 4954 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1507   class class class wbr 4929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930
This theorem is referenced by:  3brtr4i  4959  ensn1  8370  1sdom2  8512  dju1p1e2ALT  9398  infmap2  9438  0lt1sr  10315  0le2  11549  2pos  11550  3pos  11552  4pos  11554  5pos  11556  6pos  11557  7pos  11558  8pos  11559  9pos  11560  1lt2  11618  2lt3  11619  3lt4  11621  4lt5  11624  5lt6  11628  6lt7  11633  7lt8  11639  8lt9  11646  nn0le2xi  11763  numltc  11938  declti  11950  xlemul1a  12497  sqge0i  13366  faclbnd2  13466  cats1fv  14083  ege2le3  15303  cos2bnd  15401  3dvdsdec  15541  n2dvdsm1  15579  n2dvds3OLD  15582  sumeven  15598  divalglem2  15606  pockthi  16099  dec2dvds  16255  prmlem1  16297  prmlem2  16309  1259prm  16325  2503prm  16329  4001prm  16334  2strstr1  16461  vitalilem5  23916  dveflem  24279  tangtx  24794  sinq12ge0  24797  cxpge0  24967  asin1  25173  birthday  25234  lgamgulmlem4  25311  ppiub  25482  bposlem7  25568  lgsdir2lem2  25604  pthdlem2  27257  ex-fl  28004  ex-ind-dvds  28018  siilem2  28406  normlem6  28671  normlem7  28672  cm2mi  29184  pjnormi  29279  unierri  29662  dp2lt10  30306  dpgti  30328  cycpm2cl  30449  cyc2fv2  30451  cycpm3cl  30453  cyc3fv3  30456  hgt750lemd  31564  hgt750lem  31567  hgt750lem2  31568  hgt750leme  31574  logi  32483  cnndvlem1  33393  taupi  34043  poimirlem25  34355  poimirlem26  34356  poimirlem27  34357  poimirlem28  34358  ftc1anclem5  34409  fdc  34459  pellfundgt1  38873  jm2.27dlem2  39000  stoweidlem13  41727  sqwvfoura  41942  sqwvfourb  41943  fourierswlem  41944  41prothprm  43150  tgblthelfgott  43346  tgoldbachlt  43347  nnlog2ge0lt1  43992
  Copyright terms: Public domain W3C validator