![]() |
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 4850 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶) |
4 | 1, 3 | mpbi 222 | 1 ⊢ 𝐴𝑅𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 class class class wbr 4842 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-rab 3097 df-v 3386 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-sn 4368 df-pr 4370 df-op 4374 df-br 4843 |
This theorem is referenced by: breqtrri 4869 3brtr3i 4871 supsrlem 10219 0lt1 10841 le9lt10 11808 9lt10 11913 hashunlei 13458 sqrt2gt1lt2 14353 trireciplem 14929 cos1bnd 15250 cos2bnd 15251 cos01gt0 15254 sin4lt0 15258 rpnnen2lem3 15278 z4even 15441 gcdaddmlem 15577 dec2dvds 16097 abvtrivd 19155 sincos4thpi 24604 log2cnv 25020 log2ublem2 25023 log2ublem3 25024 log2le1 25026 birthday 25030 harmonicbnd3 25083 lgam1 25139 basellem7 25162 ppiublem1 25276 ppiublem2 25277 ppiub 25278 bposlem4 25361 bposlem5 25362 bposlem9 25366 lgsdir2lem2 25400 lgsdir2lem3 25401 ex-fl 27825 siilem1 28224 normlem5 28489 normlem6 28490 norm-ii-i 28512 norm3adifii 28523 cmm2i 28984 mayetes3i 29106 nmopcoadji 29478 mdoc2i 29803 dmdoc2i 29805 dp2lt10 30101 dp2ltsuc 30103 dplti 30122 sqsscirc1 30463 ballotlem1c 31079 hgt750lem 31242 problem5 32071 circum 32076 bj-pinftyccb 33600 bj-minftyccb 33604 poimirlem25 33916 cntotbnd 34075 jm2.23 38337 halffl 40244 wallispi 41019 stirlinglem1 41023 fouriersw 41180 |
Copyright terms: Public domain | W3C validator |