![]() |
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 9436 | . 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 supcsup 9431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-in 3954 df-ss 3964 df-uni 4908 df-sup 9433 |
This theorem is referenced by: supsn 9463 infrenegsup 12193 supxrmnf 13292 rpsup 13827 resup 13828 gcdcom 16450 gcdass 16485 ovolgelb 24979 itg2seq 25242 itg2i1fseq 25255 itg2cnlem1 25261 dvfsumrlim 25530 pserdvlem2 25922 logtayl 26150 nmopnegi 31196 nmop0 31217 nmfn0 31218 esumnul 32984 ismblfin 36467 ovoliunnfl 36468 voliunnfl 36470 itg2addnclem 36477 binomcxplemdvsum 43047 binomcxp 43049 supxrleubrnmptf 44096 limsup0 44345 limsupresico 44351 liminfresico 44422 liminf10ex 44425 ioodvbdlimc1lem1 44582 ioodvbdlimc1 44584 ioodvbdlimc2 44586 fourierdlem41 44799 fourierdlem48 44805 fourierdlem49 44806 fourierdlem70 44827 fourierdlem71 44828 fourierdlem97 44854 fourierdlem103 44860 fourierdlem104 44861 fourierdlem109 44866 sge00 45027 sge0sn 45030 sge0xaddlem2 45085 decsmf 45418 smflimsuplem1 45471 smflimsuplem3 45473 smflimsup 45479 |
Copyright terms: Public domain | W3C validator |