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 8897 | . 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 supcsup 8892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-ral 3140 df-rex 3141 df-rab 3144 df-uni 4831 df-sup 8894 |
This theorem is referenced by: supsn 8924 infrenegsup 11612 supxrmnf 12698 rpsup 13222 resup 13223 gcdcom 15850 gcdass 15883 ovolgelb 24008 itg2seq 24270 itg2i1fseq 24283 itg2cnlem1 24289 dvfsumrlim 24555 pserdvlem2 24943 logtayl 25170 nmopnegi 29669 nmop0 29690 nmfn0 29691 esumnul 31206 ismblfin 34814 ovoliunnfl 34815 voliunnfl 34817 itg2addnclem 34824 binomcxplemdvsum 40564 binomcxp 40566 supxrleubrnmptf 41603 limsup0 41851 limsupresico 41857 liminfresico 41928 liminf10ex 41931 ioodvbdlimc1lem1 42092 ioodvbdlimc1 42094 ioodvbdlimc2 42096 fourierdlem41 42310 fourierdlem48 42316 fourierdlem49 42317 fourierdlem70 42338 fourierdlem71 42339 fourierdlem97 42365 fourierdlem103 42371 fourierdlem104 42372 fourierdlem109 42377 sge00 42535 sge0sn 42538 sge0xaddlem2 42593 decsmf 42920 smflimsuplem1 42971 smflimsuplem3 42973 smflimsup 42979 |
Copyright terms: Public domain | W3C validator |