![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breqtri | Structured version Visualization version GIF 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 5038 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶) |
4 | 1, 3 | mpbi 233 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 class class class wbr 5030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 |
This theorem is referenced by: breqtrri 5057 3brtr3i 5059 supsrlem 10522 0lt1 11151 le9lt10 12113 9lt10 12217 hashunlei 13782 sqrt2gt1lt2 14626 trireciplem 15209 cos1bnd 15532 cos2bnd 15533 cos01gt0 15536 sin4lt0 15540 rpnnen2lem3 15561 z4even 15713 gcdaddmlem 15862 dec2dvds 16389 abvtrivd 19604 sincos4thpi 25106 log2cnv 25530 log2ublem2 25533 log2ublem3 25534 log2le1 25536 birthday 25540 harmonicbnd3 25593 lgam1 25649 basellem7 25672 ppiublem1 25786 ppiub 25788 bposlem4 25871 bposlem5 25872 bposlem9 25876 lgsdir2lem2 25910 lgsdir2lem3 25911 ex-fl 28232 siilem1 28634 normlem5 28897 normlem6 28898 norm-ii-i 28920 norm3adifii 28931 cmm2i 29390 mayetes3i 29512 nmopcoadji 29884 mdoc2i 30209 dmdoc2i 30211 dp2lt10 30586 dp2ltsuc 30588 dplti 30607 sqsscirc1 31261 ballotlem1c 31875 hgt750lem 32032 problem5 33025 circum 33030 bj-pinftyccb 34636 bj-minftyccb 34640 poimirlem25 35082 cntotbnd 35234 3lexlogpow5ineq1 39341 jm2.23 39937 tr3dom 40236 halffl 41928 wallispi 42712 stirlinglem1 42716 fouriersw 42873 |
Copyright terms: Public domain | W3C validator |