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

Theorem eltopss 22279
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 4902 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 3999 . 2 (𝐴𝐽𝐴𝑋)
43adantl 483 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wss 3914   cuni 4869  Topctop 22265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931  df-uni 4870
This theorem is referenced by:  riinopn  22280  opncld  22407  ntrval2  22425  ntrss3  22434  cmclsopn  22436  opncldf1  22458  opnneissb  22488  opnssneib  22489  opnneiss  22492  neitr  22554  restntr  22556  cnpnei  22638  imasnopn  23064  cnextcn  23441  utopreg  23627  ist0cld  32478  opnregcld  34855  ptrecube  36128  poimirlem29  36157  poimir  36161  seposep  47048  iscnrm3rlem7  47069
  Copyright terms: Public domain W3C validator