Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > infeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
Ref | Expression |
---|---|
infeq1d.1 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
infeq1d | ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infeq1d.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
2 | infeq1 9116 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 infcinf 9081 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3422 df-in 3887 df-ss 3897 df-uni 4834 df-sup 9082 df-inf 9083 |
This theorem is referenced by: limsupval 15059 lcmval 16173 lcmass 16195 lcmfval 16202 lcmf0val 16203 lcmfpr 16208 odzval 16368 ramval 16585 imasval 17040 imasdsval 17044 gexval 18991 nmofval 23636 nmoval 23637 metdsval 23768 lebnumlem1 23882 lebnumlem3 23884 ovolval 24394 ovolshft 24432 ioorf 24494 mbflimsup 24587 ig1pval 25094 elqaalem1 25236 elqaalem2 25237 elqaalem3 25238 elqaa 25239 omsval 31996 omsfval 31997 ballotlemi 32203 pellfundval 40433 dgraaval 40700 supminfrnmpt 42686 infxrpnf 42688 infxrpnf2 42706 supminfxr 42707 supminfxr2 42712 supminfxrrnmpt 42714 limsupval3 42936 limsupresre 42940 limsupresico 42944 limsuppnfdlem 42945 limsupvaluz 42952 limsupvaluzmpt 42961 liminfval 43003 liminfgval 43006 liminfval5 43009 limsupresxr 43010 liminfresxr 43011 liminfval2 43012 liminfresico 43015 liminf10ex 43018 liminfvalxr 43027 fourierdlem31 43382 ovnval 43782 ovnval2 43786 ovnval2b 43793 ovolval2 43885 ovnovollem3 43899 smfinf 44051 smfinfmpt 44052 prmdvdsfmtnof1 44740 |
Copyright terms: Public domain | W3C validator |