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 9066 | . 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 supcsup 9061 |
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 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3415 df-in 3878 df-ss 3888 df-uni 4825 df-sup 9063 |
This theorem is referenced by: supsn 9093 infrenegsup 11820 supxrmnf 12912 rpsup 13444 resup 13445 gcdcom 16077 gcdass 16112 ovolgelb 24382 itg2seq 24645 itg2i1fseq 24658 itg2cnlem1 24664 dvfsumrlim 24933 pserdvlem2 25325 logtayl 25553 nmopnegi 30051 nmop0 30072 nmfn0 30073 esumnul 31733 ismblfin 35560 ovoliunnfl 35561 voliunnfl 35563 itg2addnclem 35570 binomcxplemdvsum 41654 binomcxp 41656 supxrleubrnmptf 42674 limsup0 42918 limsupresico 42924 liminfresico 42995 liminf10ex 42998 ioodvbdlimc1lem1 43155 ioodvbdlimc1 43157 ioodvbdlimc2 43159 fourierdlem41 43372 fourierdlem48 43378 fourierdlem49 43379 fourierdlem70 43400 fourierdlem71 43401 fourierdlem97 43427 fourierdlem103 43433 fourierdlem104 43434 fourierdlem109 43439 sge00 43597 sge0sn 43600 sge0xaddlem2 43655 decsmf 43982 smflimsuplem1 44033 smflimsuplem3 44035 smflimsup 44041 |
Copyright terms: Public domain | W3C validator |