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

Theorem breqtri 4465
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 4450 . 2  |-  ( A R B  <->  A R C )
41, 3mpbi 208 1  |-  A R C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374   class class class wbr 4442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443
This theorem is referenced by:  breqtrri  4467  3brtr3i  4469  supsrlem  9479  0lt1  10066  hashunlei  12437  sqr2gt1lt2  13060  trireciplem  13627  cos1bnd  13774  cos2bnd  13775  cos01gt0  13778  sin4lt0  13782  rpnnen2lem3  13802  gcdaddmlem  14016  dec2dvds  14399  abvtrivd  17267  sincos4thpi  22634  log2cnv  22998  log2ublem2  23001  log2ublem3  23002  birthday  23007  harmonicbnd3  23060  basellem7  23083  ppiublem1  23200  ppiublem2  23201  ppiub  23202  bposlem9  23290  lgsdir2lem2  23322  lgsdir2lem3  23323  ex-fl  24833  siilem1  25430  normlem5  25695  normlem6  25696  norm-ii-i  25718  norm3adifii  25729  cmm2i  26189  mayetes3i  26312  nmopcoadji  26684  mdoc2i  27009  dmdoc2i  27011  sqsscirc1  27514  log2le1  27651  ballotlem1c  28074  lgam1  28234  problem5  28486  circum  28503  cntotbnd  29884  jm2.23  30533  halffl  31027  wallispi  31327  stirlinglem1  31331  sqwvfoura  31486  sqwvfourb  31487  fourierswlem  31488  fouriersw  31489  bj-pinftyccb  33573  bj-minftyccb  33577
  Copyright terms: Public domain W3C validator