Database
REAL AND COMPLEX NUMBERS
Order sets
Real number intervals
ioossre
Next ⟩
ioosscn
Metamath Proof Explorer
Ascii
Structured
Theorem
ioossre
Description:
An open interval is a set of reals.
(Contributed by
NM
, 31-May-2007)
Ref
Expression
Assertion
ioossre
⊢
(
𝐴
(,)
𝐵
) ⊆ ℝ
Proof
Step
Hyp
Ref
Expression
1
elioore
⊢
(
𝑥
∈ (
𝐴
(,)
𝐵
) →
𝑥
∈ ℝ )
2
1
ssriv
⊢
(
𝐴
(,)
𝐵
) ⊆ ℝ