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

Theorem breqtri 4643
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 4626 . 2 (𝐴𝑅𝐵𝐴𝑅𝐶)
41, 3mpbi 220 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480   class class class wbr 4618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619
This theorem is referenced by:  breqtrri  4645  3brtr3i  4647  supsrlem  9883  0lt1  10501  le9lt10  11480  9lt10  11624  hashunlei  13159  sqrt2gt1lt2  13956  trireciplem  14526  cos1bnd  14849  cos2bnd  14850  cos01gt0  14853  sin4lt0  14857  rpnnen2lem3  14877  z4even  15039  gcdaddmlem  15176  dec2dvds  15698  abvtrivd  18768  sincos4thpi  24182  log2cnv  24584  log2ublem2  24587  log2ublem3  24588  log2le1  24590  birthday  24594  harmonicbnd3  24647  lgam1  24703  basellem7  24726  ppiublem1  24840  ppiublem2  24841  ppiub  24842  bposlem4  24925  bposlem5  24926  bposlem9  24930  lgsdir2lem2  24964  lgsdir2lem3  24965  ex-fl  27171  siilem1  27573  normlem5  27838  normlem6  27839  norm-ii-i  27861  norm3adifii  27872  cmm2i  28333  mayetes3i  28455  nmopcoadji  28827  mdoc2i  29152  dmdoc2i  29154  sqsscirc1  29754  ballotlem1c  30368  problem5  31298  circum  31303  bj-pinftyccb  32768  bj-minftyccb  32772  poimirlem25  33093  cntotbnd  33254  jm2.23  37070  halffl  38997  wallispi  39615  stirlinglem1  39619  fouriersw  39776
  Copyright terms: Public domain W3C validator