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

Theorem breqtri 4419
 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 4403 . 2
41, 3mpbi 213 1
 Colors of variables: wff setvar class Syntax hints:   wceq 1452   class class class wbr 4395 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396 This theorem is referenced by:  breqtrri  4421  3brtr3i  4423  supsrlem  9553  0lt1  10157  hashunlei  12638  sqrt2gt1lt2  13415  trireciplem  13997  cos1bnd  14318  cos2bnd  14319  cos01gt0  14322  sin4lt0  14326  rpnnen2lem3  14346  gcdaddmlem  14571  dec2dvds  15114  abvtrivd  18146  sincos4thpi  23547  log2cnv  23949  log2ublem2  23952  log2ublem3  23953  log2le1  23955  birthday  23959  harmonicbnd3  24012  lgam1  24068  basellem7  24092  ppiublem1  24209  ppiublem2  24210  ppiub  24211  bposlem9  24299  lgsdir2lem2  24331  lgsdir2lem3  24332  ex-fl  25976  siilem1  26573  normlem5  26848  normlem6  26849  norm-ii-i  26871  norm3adifii  26882  cmm2i  27341  mayetes3i  27463  nmopcoadji  27835  mdoc2i  28160  dmdoc2i  28162  sqsscirc1  28788  ballotlem1c  29413  ballotlem1cOLD  29451  problem5  30373  circum  30390  bj-pinftyccb  31733  bj-minftyccb  31737  poimirlem25  32029  cntotbnd  32192  jm2.23  35922  halffl  37601  wallispi  38044  stirlinglem1  38048  fouriersw  38207
 Copyright terms: Public domain W3C validator