Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > breqtri | Structured version Visualization version Unicode version |
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
breqtr.1 | |
breqtr.2 |
Ref | Expression |
---|---|
breqtri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breqtr.1 | . 2 | |
2 | breqtr.2 | . . 3 | |
3 | 2 | breq2i 4661 | . 2 |
4 | 1, 3 | mpbi 220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 class class class wbr 4653 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 |
This theorem is referenced by: breqtrri 4680 3brtr3i 4682 supsrlem 9932 0lt1 10550 le9lt10 11529 9lt10 11673 hashunlei 13212 sqrt2gt1lt2 14015 trireciplem 14594 cos1bnd 14917 cos2bnd 14918 cos01gt0 14921 sin4lt0 14925 rpnnen2lem3 14945 z4even 15108 gcdaddmlem 15245 dec2dvds 15767 abvtrivd 18840 sincos4thpi 24265 log2cnv 24671 log2ublem2 24674 log2ublem3 24675 log2le1 24677 birthday 24681 harmonicbnd3 24734 lgam1 24790 basellem7 24813 ppiublem1 24927 ppiublem2 24928 ppiub 24929 bposlem4 25012 bposlem5 25013 bposlem9 25017 lgsdir2lem2 25051 lgsdir2lem3 25052 ex-fl 27304 siilem1 27706 normlem5 27971 normlem6 27972 norm-ii-i 27994 norm3adifii 28005 cmm2i 28466 mayetes3i 28588 nmopcoadji 28960 mdoc2i 29285 dmdoc2i 29287 dp2lt10 29591 dp2ltsuc 29593 dplti 29613 sqsscirc1 29954 ballotlem1c 30569 hgt750lem 30729 problem5 31563 circum 31568 bj-pinftyccb 33108 bj-minftyccb 33112 poimirlem25 33434 cntotbnd 33595 jm2.23 37563 halffl 39510 wallispi 40287 stirlinglem1 40291 fouriersw 40448 |
Copyright terms: Public domain | W3C validator |