Metamath Proof Explorer


Syntax definition c2ndc

Description: Extend class definition to include the class of all second-countable topologies.

Ref Expression
Assertion c2ndc class 2ndω