![]() |
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 4693 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶) |
4 | 1, 3 | mpbi 220 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 class class class wbr 4685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 |
This theorem is referenced by: breqtrri 4712 3brtr3i 4714 supsrlem 9970 0lt1 10588 le9lt10 11567 9lt10 11711 hashunlei 13250 sqrt2gt1lt2 14059 trireciplem 14638 cos1bnd 14961 cos2bnd 14962 cos01gt0 14965 sin4lt0 14969 rpnnen2lem3 14989 z4even 15155 gcdaddmlem 15292 dec2dvds 15814 abvtrivd 18888 sincos4thpi 24310 log2cnv 24716 log2ublem2 24719 log2ublem3 24720 log2le1 24722 birthday 24726 harmonicbnd3 24779 lgam1 24835 basellem7 24858 ppiublem1 24972 ppiublem2 24973 ppiub 24974 bposlem4 25057 bposlem5 25058 bposlem9 25062 lgsdir2lem2 25096 lgsdir2lem3 25097 ex-fl 27434 siilem1 27834 normlem5 28099 normlem6 28100 norm-ii-i 28122 norm3adifii 28133 cmm2i 28594 mayetes3i 28716 nmopcoadji 29088 mdoc2i 29413 dmdoc2i 29415 dp2lt10 29719 dp2ltsuc 29721 dplti 29741 sqsscirc1 30082 ballotlem1c 30697 hgt750lem 30857 problem5 31689 circum 31694 bj-pinftyccb 33238 bj-minftyccb 33242 poimirlem25 33564 cntotbnd 33725 jm2.23 37880 halffl 39824 wallispi 40605 stirlinglem1 40609 fouriersw 40766 |
Copyright terms: Public domain | W3C validator |