| 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 9516 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 infcinf 9481 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-ss 3968 df-uni 4908 df-sup 9482 df-inf 9483 |
| This theorem is referenced by: infsn 9545 nninf 12971 nn0inf 12972 lcmcom 16630 lcmass 16651 lcmf0 16671 imasdsval2 17561 imasdsf1olem 24383 ftalem6 27121 aks4d1 42090 sticksstones2 42148 supminfxr2 45480 limsup0 45709 limsupvaluz 45723 limsupmnflem 45735 limsupvaluz2 45753 limsup10ex 45788 cnrefiisp 45845 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 elaa2 46249 etransc 46298 ioorrnopn 46320 ovnval2 46560 ovolval3 46662 vonioolem2 46696 |
| Copyright terms: Public domain | W3C validator |