| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > supeq1i | Structured version Visualization version GIF version | ||
| Description: Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
| Ref | Expression |
|---|---|
| supeq1i.1 | ⊢ 𝐵 = 𝐶 |
| Ref | Expression |
|---|---|
| supeq1i | ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | supeq1i.1 | . 2 ⊢ 𝐵 = 𝐶 | |
| 2 | supeq1 9485 | . 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 supcsup 9480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-ss 3968 df-uni 4908 df-sup 9482 |
| This theorem is referenced by: supsn 9512 infrenegsup 12251 supxrmnf 13359 rpsup 13906 resup 13907 gcdcom 16550 gcdass 16584 ovolgelb 25515 itg2seq 25777 itg2i1fseq 25790 itg2cnlem1 25796 dvfsumrlim 26072 pserdvlem2 26472 logtayl 26702 nmopnegi 31984 nmop0 32005 nmfn0 32006 esumnul 34049 ismblfin 37668 ovoliunnfl 37669 voliunnfl 37671 itg2addnclem 37678 binomcxplemdvsum 44374 binomcxp 44376 supxrleubrnmptf 45462 limsup0 45709 limsupresico 45715 liminfresico 45786 liminf10ex 45789 ioodvbdlimc1lem1 45946 ioodvbdlimc1 45948 ioodvbdlimc2 45950 fourierdlem41 46163 fourierdlem48 46169 fourierdlem49 46170 fourierdlem70 46191 fourierdlem71 46192 fourierdlem97 46218 fourierdlem103 46224 fourierdlem104 46225 fourierdlem109 46230 sge00 46391 sge0sn 46394 sge0xaddlem2 46449 decsmf 46782 smflimsuplem1 46835 smflimsuplem3 46837 smflimsup 46843 |
| Copyright terms: Public domain | W3C validator |