Theorem elicc01 13054

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 10835	. 2 ⊢ 0 ∈ ℝ
2		1re 10833	. 2 ⊢ 1 ∈ ℝ
3	1, 2	elicc2i 13001	1 ⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1))

Syntax hints:   ↔ wb 209   ∧ w3a 1089   ∈ wcel 2110   class class class wbr 5053  (class class class)co 7213  ℝcr 10728  0cc0 10729  1c1 10730   ≤ cle 10868  [,]cicc 12938

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 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-i2m1 10797  ax-1ne0 10798  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-icc 12942

This theorem is referenced by:  elunitrn  13055  0elunit  13057  1elunit  13058  divelunit  13082  lincmb01cmp  13083  iccf1o  13084  rpnnen2lem12  15786  blcvx  23695  iirev  23826  iihalf2  23830  elii2  23833  iimulcl  23834  iccpnfhmeo  23842  xrhmeo  23843  lebnumii  23863  htpycc  23877  pcocn  23914  pcohtpylem  23916  pcopt  23919  pcopt2  23920  pcoass  23921  pcorevlem  23923  vitalilem2  24506  abelth2  25334  chordthmlem4  25718  leibpi  25825  jensenlem2  25870  lgamgulmlem2  25912  ttgcontlem1  26976  brbtwn2  26996  ax5seglem1  27019  ax5seglem2  27020  ax5seglem3  27022  ax5seglem5  27024  ax5seglem6  27025  ax5seglem9  27028  ax5seg  27029  axbtwnid  27030  axpaschlem  27031  axpasch  27032  axcontlem2  27056  axcontlem4  27058  axcontlem7  27061  stge0  30305  stle1  30306  strlem3a  30333  elunitge0  31563  unitdivcld  31565  xrge0iifiso  31599  xrge0iifhom  31601  resconn  32921  snmlff  33004  poimirlem29  35543  poimirlem30  35544  poimirlem31  35545  poimirlem32  35546  i0oii  45886  io1ii  45887