HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition cnei 7709
Description: Extend class notation with neighborhood relation for topologies.
Assertion
Ref Expression
cnei class nei
See definition df-nei 7710 for more information.
Colors of variables: wff set class
Copyright terms: Public domain