Theorem infeq1i 9453

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 9451	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

This proof depends on syntax axioms:   = wceq 1570  infcinf 9415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-sup 9416  df-inf 9417

This theorem is used by:  infsn  9481  nninf  12982  nn0inf  12983  lcmcom  16689  lcmass  16710  lcmf0  16730  imasdsval2  17608  imasdsf1olem  24605  ftalem6  27322  aks4d1  42963  sticksstones2  43021  supminfxr2  46305  limsup0  46530  limsupvaluz  46544  limsupmnflem  46556  limsupvaluz2  46574  limsup10ex  46609  cnrefiisp  46666  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  elaa2  47070  etransc  47119  ioorrnopn  47141  ovnval2  47381  ovolval3  47483  vonioolem2  47517