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

Theorem breqtri 5094
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
breqtr.1 𝐴𝑅𝐵
breqtr.2 𝐵 = 𝐶
Assertion
Ref Expression
breqtri 𝐴𝑅𝐶

Proof of Theorem breqtri
StepHypRef Expression
1 breqtr.1 . 2 𝐴𝑅𝐵
2 breqtr.2 . . 3 𝐵 = 𝐶
32breq2i 5077 . 2 (𝐴𝑅𝐵𝐴𝑅𝐶)
41, 3mpbi 233 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543   class class class wbr 5069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-br 5070
This theorem is referenced by:  breqtrri  5096  3brtr3i  5098  supsrlem  10754  0lt1  11383  le9lt10  12349  9lt10  12453  hashunlei  14024  sqrt2gt1lt2  14870  trireciplem  15458  cos1bnd  15780  cos2bnd  15781  cos01gt0  15784  sin4lt0  15788  rpnnen2lem3  15809  z4even  15965  gcdaddmlem  16115  dec2dvds  16648  abvtrivd  19908  sincos4thpi  25434  log2cnv  25858  log2ublem2  25861  log2ublem3  25862  log2le1  25864  birthday  25868  harmonicbnd3  25921  lgam1  25977  basellem7  26000  ppiublem1  26114  ppiub  26116  bposlem4  26199  bposlem5  26200  bposlem9  26204  lgsdir2lem2  26238  lgsdir2lem3  26239  ex-fl  28561  siilem1  28963  normlem5  29226  normlem6  29227  norm-ii-i  29249  norm3adifii  29260  cmm2i  29719  mayetes3i  29841  nmopcoadji  30213  mdoc2i  30538  dmdoc2i  30540  dp2lt10  30909  dp2ltsuc  30911  dplti  30930  sqsscirc1  31603  ballotlem1c  32217  hgt750lem  32374  problem5  33370  circum  33375  bj-pinftyccb  35162  bj-minftyccb  35166  poimirlem25  35575  cntotbnd  35727  3lexlogpow5ineq1  39832  3lexlogpow5ineq2  39833  aks4d1p1p2  39847  aks4d1p1p7  39851  jm2.23  40568  tr3dom  40867  halffl  42555  wallispi  43331  stirlinglem1  43335  fouriersw  43492
  Copyright terms: Public domain W3C validator