MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supeq1i Structured version   Visualization version   GIF version

Theorem supeq1i 9068
Description: Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
supeq1i.1 𝐵 = 𝐶
Assertion
Ref Expression
supeq1i sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)

Proof of Theorem supeq1i
StepHypRef Expression
1 supeq1i.1 . 2 𝐵 = 𝐶
2 supeq1 9066 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2ax-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