Theorem infeq1i 9094

Description: Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)

Hypothesis

Ref	Expression
infeq1i.1	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
infeq1i	⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Proof of Theorem infeq1i

Step	Hyp	Ref	Expression
1		infeq1i.1	. 2 ⊢ 𝐵 = 𝐶
2		infeq1 9092	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Syntax hints:   = wceq 1543  infcinf 9057

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 3410  df-in 3873  df-ss 3883  df-uni 4820  df-sup 9058  df-inf 9059

This theorem is referenced by:  infsn  9121  nninf  12525  nn0inf  12526  lcmcom  16150  lcmass  16171  lcmf0  16191  imasdsval2  17021  imasdsf1olem  23271  ftalem6  25960  sticksstones2  39825  supminfxr2  42684  limsup0  42910  limsupvaluz  42924  limsupmnflem  42936  limsupvaluz2  42954  limsup10ex  42989  cnrefiisp  43046  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  elaa2  43450  etransc  43499  ioorrnopn  43521  ovnval2  43758  ovolval3  43860  vonioolem2  43894