![]() |
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 8622 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 infcinf 8587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ral 3092 df-rex 3093 df-rab 3096 df-uni 4627 df-sup 8588 df-inf 8589 |
This theorem is referenced by: infsn 8650 nninf 12010 nn0inf 12011 lcmcom 15637 lcmass 15658 lcmf0 15678 imasdsval2 16487 imasdsf1olem 22502 ftalem6 25152 supminfxr2 40429 limsup0 40657 limsupvaluz 40671 limsupmnflem 40683 limsupvaluz2 40701 limsup10ex 40736 cnrefiisp 40787 ioodvbdlimc1lem2 40878 ioodvbdlimc2lem 40880 elaa2 41181 etransc 41230 ioorrnopn 41255 ovnval2 41492 ovolval3 41594 vonioolem2 41628 |
Copyright terms: Public domain | W3C validator |