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

Theorem supeq1i 8509
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 8507 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  supcsup 8502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-uni 4575  df-sup 8504
This theorem is referenced by:  supsn  8534  infrenegsup  11208  supxrmnf  12352  rpsup  12873  resup  12874  gcdcom  15443  gcdass  15472  ovolgelb  23468  itg2seq  23729  itg2i1fseq  23742  itg2cnlem1  23748  dvfsumrlim  24014  pserdvlem2  24402  logtayl  24627  nmopnegi  29164  nmop0  29185  nmfn0  29186  esumnul  30450  ismblfin  33783  ovoliunnfl  33784  voliunnfl  33786  itg2addnclem  33793  binomcxplemdvsum  39080  binomcxp  39082  supxrleubrnmptf  40196  limsup0  40444  limsupresico  40450  liminfresico  40521  liminf10ex  40524  ioodvbdlimc1lem1  40664  ioodvbdlimc1  40666  ioodvbdlimc2  40668  fourierdlem41  40882  fourierdlem48  40888  fourierdlem49  40889  fourierdlem70  40910  fourierdlem71  40911  fourierdlem97  40937  fourierdlem103  40943  fourierdlem104  40944  fourierdlem109  40949  sge00  41110  sge0sn  41113  sge0xaddlem2  41168  decsmf  41495  smflimsuplem1  41546  smflimsuplem3  41548  smflimsup  41554
  Copyright terms: Public domain W3C validator