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

Theorem eltopss 21039
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 4660 . . 3 (𝐴𝐽𝐴 𝐽)
2 1open.1 . . 3 𝑋 = 𝐽
31, 2syl6sseqr 3849 . 2 (𝐴𝐽𝐴𝑋)
43adantl 474 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  wcel 2157  wss 3770   cuni 4629  Topctop 21025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-v 3388  df-in 3777  df-ss 3784  df-uni 4630
This theorem is referenced by:  riinopn  21040  opncld  21165  ntrval2  21183  ntrss3  21192  cmclsopn  21194  opncldf1  21216  opnneissb  21246  opnssneib  21247  opnneiss  21250  neitr  21312  restntr  21314  cnpnei  21396  imasnopn  21821  cnextcn  22198  utopreg  22383  opnregcld  32836  ptrecube  33897  poimirlem29  33926  poimir  33930
  Copyright terms: Public domain W3C validator