Theorem infeq1i 9475

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

This proof depends on syntax axioms:   = wceq 1569  infcinf 9437

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-sup 9438  df-inf 9439

This theorem is used by:  infsn  9503  nninf  13060  nn0inf  13061  lcmcom  16774  lcmass  16795  lcmf0  16815  imasdsval2  17694  imasdsf1olem  24698  ftalem6  27411  aks4d1  43233  sticksstones2  43291  supminfxr2  46573  limsup0  46798  limsupvaluz  46812  limsupmnflem  46824  limsupvaluz2  46842  limsup10ex  46877  cnrefiisp  46934  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  elaa2  47338  etransc  47387  ioorrnopn  47409  ovnval2  47649  ovolval3  47751  vonioolem2  47785