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

Theorem supeq1i 8903
 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 8901 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530  supcsup 8896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-ral 3141  df-rex 3142  df-rab 3145  df-uni 4831  df-sup 8898 This theorem is referenced by:  supsn  8928  infrenegsup  11616  supxrmnf  12702  rpsup  13226  resup  13227  gcdcom  15854  gcdass  15887  ovolgelb  24073  itg2seq  24335  itg2i1fseq  24348  itg2cnlem1  24354  dvfsumrlim  24620  pserdvlem2  25008  logtayl  25235  nmopnegi  29734  nmop0  29755  nmfn0  29756  esumnul  31295  ismblfin  34920  ovoliunnfl  34921  voliunnfl  34923  itg2addnclem  34930  binomcxplemdvsum  40672  binomcxp  40674  supxrleubrnmptf  41711  limsup0  41959  limsupresico  41965  liminfresico  42036  liminf10ex  42039  ioodvbdlimc1lem1  42200  ioodvbdlimc1  42202  ioodvbdlimc2  42204  fourierdlem41  42418  fourierdlem48  42424  fourierdlem49  42425  fourierdlem70  42446  fourierdlem71  42447  fourierdlem97  42473  fourierdlem103  42479  fourierdlem104  42480  fourierdlem109  42485  sge00  42643  sge0sn  42646  sge0xaddlem2  42701  decsmf  43028  smflimsuplem1  43079  smflimsuplem3  43081  smflimsup  43087
 Copyright terms: Public domain W3C validator