| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elicc01 | Structured version Visualization version GIF version | ||
| Description: Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022.) |
| Ref | Expression |
|---|---|
| elicc01 | ⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0re 11152 | . 2 ⊢ 0 ∈ ℝ | |
| 2 | 1re 11150 | . 2 ⊢ 1 ∈ ℝ | |
| 3 | 1, 2 | elicc2i 13349 | 1 ⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5102 (class class class)co 7369 ℝcr 11043 0cc0 11044 1c1 11045 ≤ cle 11185 [,]cicc 13285 |
| 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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-i2m1 11112 ax-1ne0 11113 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-icc 13289 |
| This theorem is referenced by: elunitrn 13404 0elunit 13406 1elunit 13407 divelunit 13431 lincmb01cmp 13432 iccf1o 13433 rpnnen2lem12 16169 blcvx 24662 iirev 24799 iihalf2 24804 elii2 24808 iimulcl 24809 iccpnfhmeo 24819 xrhmeo 24820 lebnumii 24841 htpycc 24855 pcocn 24893 pcohtpylem 24895 pcopt 24898 pcopt2 24899 pcoass 24900 pcorevlem 24902 vitalilem2 25486 abelth2 26328 chordthmlem4 26721 leibpi 26828 jensenlem2 26874 lgamgulmlem2 26916 ttgcontlem1 28788 brbtwn2 28808 ax5seglem1 28831 ax5seglem2 28832 ax5seglem3 28834 ax5seglem5 28836 ax5seglem6 28837 ax5seglem9 28840 ax5seg 28841 axbtwnid 28842 axpaschlem 28843 axpasch 28844 axcontlem2 28868 axcontlem4 28870 axcontlem7 28873 stge0 32126 stle1 32127 strlem3a 32154 elunitge0 33862 unitdivcld 33864 xrge0iifiso 33898 xrge0iifhom 33900 resconn 35206 snmlff 35289 poimirlem29 37616 poimirlem30 37617 poimirlem31 37618 poimirlem32 37619 i0oii 48881 io1ii 48882 |
| Copyright terms: Public domain | W3C validator |