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

Theorem breqtrri 4823
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 2761 . 2 𝐵 = 𝐶
41, 3breqtri 4821 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624   class class class wbr 4796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797
This theorem is referenced by:  3brtr4i  4826  ensn1  8177  1sdom2  8316  pm110.643ALT  9184  infmap2  9224  0lt1sr  10100  0le2  11295  2pos  11296  3pos  11298  4pos  11300  5pos  11302  6pos  11303  7pos  11304  8pos  11305  9pos  11306  10posOLD  11307  1lt2  11378  2lt3  11379  3lt4  11381  4lt5  11384  5lt6  11388  6lt7  11393  7lt8  11399  8lt9  11406  9lt10OLD  11414  nn0le2xi  11531  numltc  11712  declti  11730  decltiOLD  11732  xlemul1a  12303  sqge0i  13137  faclbnd2  13264  cats1fv  13796  ege2le3  15011  cos2bnd  15109  3dvdsdec  15248  3dvdsdecOLD  15249  n2dvdsm1  15299  n2dvds3  15301  sumeven  15304  divalglem2  15312  pockthi  15805  dec2dvds  15961  prmlem1  16008  prmlem2  16021  1259prm  16037  2503prm  16041  4001prm  16046  2strstr1  16180  vitalilem5  23572  dveflem  23933  tangtx  24448  sinq12ge0  24451  cxpge0  24620  asin1  24812  birthday  24872  lgamgulmlem4  24949  ppiub  25120  bposlem7  25206  lgsdir2lem2  25242  pthdlem2  26866  ex-fl  27607  ex-ind-dvds  27621  siilem2  28008  normlem6  28273  normlem7  28274  cm2mi  28786  pjnormi  28881  unierri  29264  dp2lt10  29892  dpgti  29915  hgt750lemd  31027  hgt750lem  31030  hgt750lem2  31031  hgt750leme  31037  logi  31919  cnndvlem1  32826  taupi  33472  poimirlem25  33739  poimirlem26  33740  poimirlem27  33741  poimirlem28  33742  ftc1anclem5  33794  fdc  33846  pellfundgt1  37941  jm2.27dlem2  38071  stoweidlem13  40725  sqwvfoura  40940  sqwvfourb  40941  fourierswlem  40942  41prothprm  42038  tgblthelfgott  42205  tgoldbachlt  42206  tgblthelfgottOLD  42211  tgoldbachltOLD  42212  nnlog2ge0lt1  42862
  Copyright terms: Public domain W3C validator