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

Theorem breqtri 4336
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 4321 . 2  |-  ( A R B  <->  A R C )
41, 3mpbi 208 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   class class class wbr 4313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314
This theorem is referenced by:  breqtrri  4338  3brtr3i  4340  supsrlem  9299  0lt1  9883  hashunlei  12196  sqr2gt1lt2  12785  trireciplem  13345  cos1bnd  13492  cos2bnd  13493  cos01gt0  13496  sin4lt0  13500  rpnnen2lem3  13520  gcdaddmlem  13733  dec2dvds  14113  abvtrivd  16947  sincos4thpi  21997  log2cnv  22361  log2ublem2  22364  log2ublem3  22365  birthday  22370  harmonicbnd3  22423  basellem7  22446  ppiublem1  22563  ppiublem2  22564  ppiub  22565  bposlem9  22653  lgsdir2lem2  22685  lgsdir2lem3  22686  ex-fl  23676  siilem1  24273  normlem5  24538  normlem6  24539  norm-ii-i  24561  norm3adifii  24572  cmm2i  25032  mayetes3i  25155  nmopcoadji  25527  mdoc2i  25852  dmdoc2i  25854  sqsscirc1  26360  log2le1  26488  ballotlem1c  26912  lgam1  27072  problem5  27324  circum  27341  cntotbnd  28721  jm2.23  29371  wallispi  29891  stirlinglem1  29895  bj-pinftyccb  32640  bj-minftyccb  32644
  Copyright terms: Public domain W3C validator