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

Theorem breqtrri 4600
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 2614 . 2 𝐵 = 𝐶
41, 3breqtri 4598 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474   class class class wbr 4573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574
This theorem is referenced by:  3brtr4i  4603  ensn1  7879  1sdom2  8017  pm110.643ALT  8856  infmap2  8896  0lt1sr  9768  0le2  10954  2pos  10955  3pos  10957  4pos  10959  5pos  10961  6pos  10962  7pos  10963  8pos  10964  9pos  10965  10posOLD  10966  1lt2  11037  2lt3  11038  3lt4  11040  4lt5  11043  5lt6  11047  6lt7  11052  7lt8  11058  8lt9  11065  9lt10OLD  11073  nn0le2xi  11190  numltc  11356  declti  11374  decltiOLD  11376  xlemul1a  11943  sqge0i  12764  faclbnd2  12891  cats1fv  13397  ege2le3  14601  cos2bnd  14699  3dvdsdec  14834  3dvdsdecOLD  14835  n2dvdsm1  14885  n2dvds3  14887  sumeven  14890  divalglem2  14898  pockthi  15391  dec2dvds  15547  prmlem1  15594  prmlem2  15607  1259prm  15623  2503prm  15627  4001prm  15632  2strstr1  15754  vitalilem5  23100  dveflem  23459  tangtx  23974  sinq12ge0  23977  cxpge0  24142  asin1  24334  birthday  24394  lgamgulmlem4  24471  ppiub  24642  bposlem7  24728  lgsdir2lem2  24764  ex-fl  26458  ex-ind-dvds  26472  siilem2  26893  normlem6  27158  normlem7  27159  cm2mi  27671  pjnormi  27766  unierri  28149  logi  30675  cnndvlem1  31500  taupi  32145  poimirlem25  32403  poimirlem26  32404  poimirlem27  32405  poimirlem28  32406  ftc1anclem5  32458  fdc  32510  pellfundgt1  36264  jm2.27dlem2  36394  stoweidlem13  38706  sqwvfoura  38921  sqwvfourb  38922  fourierswlem  38923  41prothprm  39875  tgblthelfgott  40030  tgoldbachlt  40031  tgblthelfgottOLD  40037  tgoldbachltOLD  40038  pthdlem2  40972  nnlog2ge0lt1  42156
  Copyright terms: Public domain W3C validator