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

Theorem breqtri 5067
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 5050 . 2 (𝐴𝑅𝐵𝐴𝑅𝐶)
41, 3mpbi 232 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537   class class class wbr 5042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043
This theorem is referenced by:  breqtrri  5069  3brtr3i  5071  supsrlem  10511  0lt1  11140  le9lt10  12104  9lt10  12208  hashunlei  13771  sqrt2gt1lt2  14614  trireciplem  15197  cos1bnd  15520  cos2bnd  15521  cos01gt0  15524  sin4lt0  15528  rpnnen2lem3  15549  z4even  15701  gcdaddmlem  15850  dec2dvds  16377  abvtrivd  19587  sincos4thpi  25085  log2cnv  25509  log2ublem2  25512  log2ublem3  25513  log2le1  25515  birthday  25519  harmonicbnd3  25572  lgam1  25628  basellem7  25651  ppiublem1  25765  ppiub  25767  bposlem4  25850  bposlem5  25851  bposlem9  25855  lgsdir2lem2  25889  lgsdir2lem3  25890  ex-fl  28211  siilem1  28613  normlem5  28876  normlem6  28877  norm-ii-i  28899  norm3adifii  28910  cmm2i  29369  mayetes3i  29491  nmopcoadji  29863  mdoc2i  30188  dmdoc2i  30190  dp2lt10  30547  dp2ltsuc  30549  dplti  30568  sqsscirc1  31159  ballotlem1c  31773  hgt750lem  31930  problem5  32920  circum  32925  bj-pinftyccb  34520  bj-minftyccb  34524  poimirlem25  34958  cntotbnd  35110  jm2.23  39730  tr3dom  40029  halffl  41717  wallispi  42503  stirlinglem1  42507  fouriersw  42664
  Copyright terms: Public domain W3C validator