Metamath Proof Explorer

Theorem eltopss

Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006)

Ref Expression
Hypothesis 1open.1 X = J
Assertion eltopss J Top A J A X


Step Hyp Ref Expression
1 1open.1 X = J
2 elssuni A J A J
3 2 1 sseqtrrdi A J A X
4 3 adantl J Top A J A X