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

Theorem breqtrri 4671
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 2629 . 2 𝐵 = 𝐶
41, 3breqtri 4669 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481   class class class wbr 4644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645
This theorem is referenced by:  3brtr4i  4674  ensn1  8005  1sdom2  8144  pm110.643ALT  8985  infmap2  9025  0lt1sr  9901  0le2  11096  2pos  11097  3pos  11099  4pos  11101  5pos  11103  6pos  11104  7pos  11105  8pos  11106  9pos  11107  10posOLD  11108  1lt2  11179  2lt3  11180  3lt4  11182  4lt5  11185  5lt6  11189  6lt7  11194  7lt8  11200  8lt9  11207  9lt10OLD  11215  nn0le2xi  11332  numltc  11513  declti  11531  decltiOLD  11533  xlemul1a  12103  sqge0i  12934  faclbnd2  13061  cats1fv  13585  ege2le3  14801  cos2bnd  14899  3dvdsdec  15035  3dvdsdecOLD  15036  n2dvdsm1  15086  n2dvds3  15088  sumeven  15091  divalglem2  15099  pockthi  15592  dec2dvds  15748  prmlem1  15795  prmlem2  15808  1259prm  15824  2503prm  15828  4001prm  15833  2strstr1  15967  vitalilem5  23362  dveflem  23723  tangtx  24238  sinq12ge0  24241  cxpge0  24410  asin1  24602  birthday  24662  lgamgulmlem4  24739  ppiub  24910  bposlem7  24996  lgsdir2lem2  25032  pthdlem2  26645  ex-fl  27274  ex-ind-dvds  27288  siilem2  27677  normlem6  27942  normlem7  27943  cm2mi  28455  pjnormi  28550  unierri  28933  dp2lt10  29565  dpgti  29588  hgt750lemd  30700  hgt750lem  30703  hgt750lem2  30704  hgt750leme  30710  logi  31595  cnndvlem1  32503  taupi  33140  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem28  33408  ftc1anclem5  33460  fdc  33512  pellfundgt1  37266  jm2.27dlem2  37396  stoweidlem13  39993  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  41prothprm  41301  tgblthelfgott  41468  tgoldbachlt  41469  tgblthelfgottOLD  41474  tgoldbachltOLD  41475  nnlog2ge0lt1  42125
  Copyright terms: Public domain W3C validator