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

Theorem breqtri 4440
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
breqtr.1  |-  A R B
breqtr.2  |-  B  =  C
Assertion
Ref Expression
breqtri  |-  A R C

Proof of Theorem breqtri
StepHypRef Expression
1 breqtr.1 . 2  |-  A R B
2 breqtr.2 . . 3  |-  B  =  C
32breq2i 4425 . 2  |-  ( A R B  <->  A R C )
41, 3mpbi 211 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   class class class wbr 4417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418
This theorem is referenced by:  breqtrri  4442  3brtr3i  4444  supsrlem  9524  0lt1  10125  hashunlei  12581  sqrt2gt1lt2  13306  trireciplem  13887  cos1bnd  14208  cos2bnd  14209  cos01gt0  14212  sin4lt0  14216  rpnnen2lem3  14236  gcdaddmlem  14455  dec2dvds  14987  abvtrivd  17996  sincos4thpi  23330  log2cnv  23732  log2ublem2  23735  log2ublem3  23736  log2le1  23738  birthday  23742  harmonicbnd3  23795  lgam1  23851  basellem7  23873  ppiublem1  23990  ppiublem2  23991  ppiub  23992  bposlem9  24080  lgsdir2lem2  24112  lgsdir2lem3  24113  ex-fl  25739  siilem1  26334  normlem5  26599  normlem6  26600  norm-ii-i  26622  norm3adifii  26633  cmm2i  27092  mayetes3i  27214  nmopcoadji  27586  mdoc2i  27911  dmdoc2i  27913  sqsscirc1  28550  ballotlem1c  29163  problem5  30086  circum  30103  bj-pinftyccb  31405  bj-minftyccb  31409  poimirlem25  31669  cntotbnd  31832  jm2.23  35561  halffl  37126  wallispi  37505  stirlinglem1  37509  fouriersw  37667
  Copyright terms: Public domain W3C validator