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

Theorem infeq1d 9117
Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
Hypothesis
Ref Expression
infeq1d.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
infeq1d (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Proof of Theorem infeq1d
StepHypRef Expression
1 infeq1d.1 . 2 (𝜑𝐵 = 𝐶)
2 infeq1 9116 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  infcinf 9081
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 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-in 3887  df-ss 3897  df-uni 4834  df-sup 9082  df-inf 9083
This theorem is referenced by:  limsupval  15059  lcmval  16173  lcmass  16195  lcmfval  16202  lcmf0val  16203  lcmfpr  16208  odzval  16368  ramval  16585  imasval  17040  imasdsval  17044  gexval  18991  nmofval  23636  nmoval  23637  metdsval  23768  lebnumlem1  23882  lebnumlem3  23884  ovolval  24394  ovolshft  24432  ioorf  24494  mbflimsup  24587  ig1pval  25094  elqaalem1  25236  elqaalem2  25237  elqaalem3  25238  elqaa  25239  omsval  31996  omsfval  31997  ballotlemi  32203  pellfundval  40433  dgraaval  40700  supminfrnmpt  42686  infxrpnf  42688  infxrpnf2  42706  supminfxr  42707  supminfxr2  42712  supminfxrrnmpt  42714  limsupval3  42936  limsupresre  42940  limsupresico  42944  limsuppnfdlem  42945  limsupvaluz  42952  limsupvaluzmpt  42961  liminfval  43003  liminfgval  43006  liminfval5  43009  limsupresxr  43010  liminfresxr  43011  liminfval2  43012  liminfresico  43015  liminf10ex  43018  liminfvalxr  43027  fourierdlem31  43382  ovnval  43782  ovnval2  43786  ovnval2b  43793  ovolval2  43885  ovnovollem3  43899  smfinf  44051  smfinfmpt  44052  prmdvdsfmtnof1  44740
  Copyright terms: Public domain W3C validator