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