Theorem infeq1i 9449

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-ss 3925  df-uni 4878  df-sup 9412  df-inf 9413

This theorem is used by:  infsn  9477  nninf  12971  nn0inf  12972  lcmcom  16676  lcmass  16697  lcmf0  16717  imasdsval2  17595  imasdsf1olem  24567  ftalem6  27279  aks4d1  42897  sticksstones2  42955  supminfxr2  46224  limsup0  46449  limsupvaluz  46463  limsupmnflem  46475  limsupvaluz2  46493  limsup10ex  46528  cnrefiisp  46585  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  elaa2  46989  etransc  47038  ioorrnopn  47060  ovnval2  47300  ovolval3  47402  vonioolem2  47436