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

Theorem breqtri 4303
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
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 4288 . 2  |-  ( A R B  <->  A R C )
41, 3mpbi 208 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  breqtrri  4305  3brtr3i  4307  supsrlem  9266  0lt1  9850  hashunlei  12159  sqr2gt1lt2  12748  trireciplem  13307  cos1bnd  13454  cos2bnd  13455  cos01gt0  13458  sin4lt0  13462  rpnnen2lem3  13482  gcdaddmlem  13695  dec2dvds  14075  abvtrivd  16849  sincos4thpi  21860  log2cnv  22224  log2ublem2  22227  log2ublem3  22228  birthday  22233  harmonicbnd3  22286  basellem7  22309  ppiublem1  22426  ppiublem2  22427  ppiub  22428  bposlem9  22516  lgsdir2lem2  22548  lgsdir2lem3  22549  ex-fl  23477  siilem1  24074  normlem5  24339  normlem6  24340  norm-ii-i  24362  norm3adifii  24373  cmm2i  24833  mayetes3i  24956  nmopcoadji  25328  mdoc2i  25653  dmdoc2i  25655  sqsscirc1  26192  log2le1  26320  ballotlem1c  26738  lgam1  26898  problem5  27150  circum  27166  cntotbnd  28539  jm2.23  29190  wallispi  29711  stirlinglem1  29715  bj-pinftyccb  32124  bj-minftyccb  32128
  Copyright terms: Public domain W3C validator