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 AB

Proof

Step Hyp Ref Expression
1 ioossre AB
2 ax-resscn
3 1 2 sstri AB