Theorem infeq1i 9455

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-ss 3916  df-uni 4868  df-sup 9418  df-inf 9419

This theorem is used by:  infsn  9483  nninf  13037  nn0inf  13038  lcmcom  16748  lcmass  16769  lcmf0  16789  imasdsval2  17668  imasdsf1olem  24672  ftalem6  27387  aks4d1  43107  sticksstones2  43165  supminfxr2  46423  limsup0  46648  limsupvaluz  46662  limsupmnflem  46674  limsupvaluz2  46692  limsup10ex  46727  cnrefiisp  46784  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  elaa2  47188  etransc  47237  ioorrnopn  47259  ovnval2  47499  ovolval3  47601  vonioolem2  47635