Metamath Proof Explorer

Theorem elicc01

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
Assertion elicc01 ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1re ⊢ 1 ∈ ℝ
3 1 2 elicc2i ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 ≤ X ∧ X ≤ 1