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

Theorem eltopss 22408
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 4941 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 4033 . 2 (𝐴𝐽𝐴𝑋)
43adantl 482 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wss 3948   cuni 4908  Topctop 22394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909
This theorem is referenced by:  riinopn  22409  opncld  22536  ntrval2  22554  ntrss3  22563  cmclsopn  22565  opncldf1  22587  opnneissb  22617  opnssneib  22618  opnneiss  22621  neitr  22683  restntr  22685  cnpnei  22767  imasnopn  23193  cnextcn  23570  utopreg  23756  ist0cld  32808  opnregcld  35210  ptrecube  36483  poimirlem29  36512  poimir  36516  seposep  47548  iscnrm3rlem7  47569
  Copyright terms: Public domain W3C validator