Theorem elicc01 13268

Description: Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022.)

Assertion

Ref	Expression
elicc01	⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1))

Proof of Theorem elicc01

Step	Hyp	Ref	Expression
1		0re 11047	. 2 ⊢ 0 ∈ ℝ
2		1re 11045	. 2 ⊢ 1 ∈ ℝ
3	1, 2	elicc2i 13215	1 ⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1))

Syntax hints:   ↔ wb 205   ∧ w3a 1086   ∈ wcel 2105   class class class wbr 5085  (class class class)co 7313  ℝcr 10940  0cc0 10941  1c1 10942   ≤ cle 11080  [,]cicc 13152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-i2m1 11009  ax-1ne0 11010  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-po 5519  df-so 5520  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-ov 7316  df-oprab 7317  df-mpo 7318  df-er 8544  df-en 8780  df-dom 8781  df-sdom 8782  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-icc 13156

This theorem is referenced by:  elunitrn  13269  0elunit  13271  1elunit  13272  divelunit  13296  lincmb01cmp  13297  iccf1o  13298  rpnnen2lem12  16003  blcvx  24032  iirev  24163  iihalf2  24167  elii2  24170  iimulcl  24171  iccpnfhmeo  24179  xrhmeo  24180  lebnumii  24200  htpycc  24214  pcocn  24251  pcohtpylem  24253  pcopt  24256  pcopt2  24257  pcoass  24258  pcorevlem  24260  vitalilem2  24844  abelth2  25672  chordthmlem4  26056  leibpi  26163  jensenlem2  26208  lgamgulmlem2  26250  ttgcontlem1  27360  brbtwn2  27381  ax5seglem1  27404  ax5seglem2  27405  ax5seglem3  27407  ax5seglem5  27409  ax5seglem6  27410  ax5seglem9  27413  ax5seg  27414  axbtwnid  27415  axpaschlem  27416  axpasch  27417  axcontlem2  27441  axcontlem4  27443  axcontlem7  27446  stge0  30694  stle1  30695  strlem3a  30722  elunitge0  31955  unitdivcld  31957  xrge0iifiso  31991  xrge0iifhom  31993  resconn  33314  snmlff  33397  poimirlem29  35866  poimirlem30  35867  poimirlem31  35868  poimirlem32  35869  i0oii  46472  io1ii  46473