Metamath Proof Explorer


Theorem ioosscn

Description: An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioosscn ⊢ A B ⊆ ℂ

Proof

Step Hyp Ref Expression
1 ioossre ⊢ A B ⊆ ℝ
2 ax-resscn ⊢ ℝ ⊆ ℂ
3 1 2 sstri ⊢ A B ⊆ ℂ