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 8928 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 infcinf 8893 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-ral 3140 df-rex 3141 df-rab 3144 df-uni 4831 df-sup 8894 df-inf 8895 |
This theorem is referenced by: infsn 8957 nninf 12317 nn0inf 12318 lcmcom 15925 lcmass 15946 lcmf0 15966 imasdsval2 16777 imasdsf1olem 22910 ftalem6 25582 supminfxr2 41621 limsup0 41851 limsupvaluz 41865 limsupmnflem 41877 limsupvaluz2 41895 limsup10ex 41930 cnrefiisp 41987 ioodvbdlimc1lem2 42093 ioodvbdlimc2lem 42095 elaa2 42396 etransc 42445 ioorrnopn 42467 ovnval2 42704 ovolval3 42806 vonioolem2 42840 |
Copyright terms: Public domain | W3C validator |