Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eltopss Structured version   Visualization version   GIF version

Theorem eltopss 20632
 Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
Hypothesis
Ref Expression
1open.1 𝑋 = 𝐽
Assertion
Ref Expression
eltopss ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)

Proof of Theorem eltopss
StepHypRef Expression
1 elssuni 4438 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2syl6sseqr 3636 . 2 (𝐴𝐽𝐴𝑋)
43adantl 482 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1992   ⊆ wss 3560  ∪ cuni 4407  Topctop 20612 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-in 3567  df-ss 3574  df-uni 4408 This theorem is referenced by:  riinopn  20633  opncld  20742  ntrval2  20760  ntrss3  20769  cmclsopn  20771  opncldf1  20793  opnneissb  20823  opnssneib  20824  opnneiss  20827  neitr  20889  restntr  20891  cnpnei  20973  imasnopn  21398  cnextcn  21776  utopreg  21961  opnregcld  31959  ptrecube  33027  poimirlem29  33056  poimir  33060
 Copyright terms: Public domain W3C validator