Metamath Proof Explorer


Theorem eliccxr

Description: A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliccxr ⊢ A ∈ B C → A ∈ ℝ *

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ B C ⊆ ℝ *
2 1 sseli ⊢ A ∈ B C → A ∈ ℝ *