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

Theorem eltopss 21651
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 4825 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2sseqtrrdi 3926 . 2 (𝐴𝐽𝐴𝑋)
43adantl 485 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2113  wss 3841   cuni 4793  Topctop 21637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-uni 4794
This theorem is referenced by:  riinopn  21652  opncld  21777  ntrval2  21795  ntrss3  21804  cmclsopn  21806  opncldf1  21828  opnneissb  21858  opnssneib  21859  opnneiss  21862  neitr  21924  restntr  21926  cnpnei  22008  imasnopn  22434  cnextcn  22811  utopreg  22997  ist0cld  31347  opnregcld  34149  ptrecube  35389  poimirlem29  35418  poimir  35422  seposep  45725  iscnrm3rlem7  45746
  Copyright terms: Public domain W3C validator