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