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 5077 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶) |
4 | 1, 3 | mpbi 233 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 class class class wbr 5069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-nul 4254 df-if 4456 df-sn 4558 df-pr 4560 df-op 4564 df-br 5070 |
This theorem is referenced by: breqtrri 5096 3brtr3i 5098 supsrlem 10754 0lt1 11383 le9lt10 12349 9lt10 12453 hashunlei 14024 sqrt2gt1lt2 14870 trireciplem 15458 cos1bnd 15780 cos2bnd 15781 cos01gt0 15784 sin4lt0 15788 rpnnen2lem3 15809 z4even 15965 gcdaddmlem 16115 dec2dvds 16648 abvtrivd 19908 sincos4thpi 25434 log2cnv 25858 log2ublem2 25861 log2ublem3 25862 log2le1 25864 birthday 25868 harmonicbnd3 25921 lgam1 25977 basellem7 26000 ppiublem1 26114 ppiub 26116 bposlem4 26199 bposlem5 26200 bposlem9 26204 lgsdir2lem2 26238 lgsdir2lem3 26239 ex-fl 28561 siilem1 28963 normlem5 29226 normlem6 29227 norm-ii-i 29249 norm3adifii 29260 cmm2i 29719 mayetes3i 29841 nmopcoadji 30213 mdoc2i 30538 dmdoc2i 30540 dp2lt10 30909 dp2ltsuc 30911 dplti 30930 sqsscirc1 31603 ballotlem1c 32217 hgt750lem 32374 problem5 33370 circum 33375 bj-pinftyccb 35162 bj-minftyccb 35166 poimirlem25 35575 cntotbnd 35727 3lexlogpow5ineq1 39832 3lexlogpow5ineq2 39833 aks4d1p1p2 39847 aks4d1p1p7 39851 jm2.23 40568 tr3dom 40867 halffl 42555 wallispi 43331 stirlinglem1 43335 fouriersw 43492 |
Copyright terms: Public domain | W3C validator |