![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > infeq1i | Structured version Visualization version GIF version |
Description: Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
Ref | Expression |
---|---|
infeq1i.1 | ⊢ 𝐵 = 𝐶 |
Ref | Expression |
---|---|
infeq1i | ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infeq1i.1 | . 2 ⊢ 𝐵 = 𝐶 | |
2 | infeq1 9499 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 infcinf 9464 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-in 3954 df-ss 3964 df-uni 4909 df-sup 9465 df-inf 9466 |
This theorem is referenced by: infsn 9528 nninf 12943 nn0inf 12944 lcmcom 16563 lcmass 16584 lcmf0 16604 imasdsval2 17497 imasdsf1olem 24278 ftalem6 27009 aks4d1 41560 sticksstones2 41619 supminfxr2 44851 limsup0 45082 limsupvaluz 45096 limsupmnflem 45108 limsupvaluz2 45126 limsup10ex 45161 cnrefiisp 45218 ioodvbdlimc1lem2 45320 ioodvbdlimc2lem 45322 elaa2 45622 etransc 45671 ioorrnopn 45693 ovnval2 45933 ovolval3 46035 vonioolem2 46069 |
Copyright terms: Public domain | W3C validator |