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

Theorem elelpwi 4610
Description: If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.)
Assertion
Ref Expression
elelpwi ((𝐴𝐵𝐵 ∈ 𝒫 𝐶) → 𝐴𝐶)

Proof of Theorem elelpwi
StepHypRef Expression
1 elpwi 4607 . . 3 (𝐵 ∈ 𝒫 𝐶𝐵𝐶)
21sseld 3982 . 2 (𝐵 ∈ 𝒫 𝐶 → (𝐴𝐵𝐴𝐶))
32impcom 407 1 ((𝐴𝐵𝐵 ∈ 𝒫 𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  𝒫 cpw 4600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602
This theorem is referenced by:  unipw  5455  axdc2lem  10488  axdc3lem4  10493  homarel  18081  txdis  23640  uhgredgrnv  29147  fpwrelmap  32744  insiga  34138  measinblem  34221  ddemeas  34237  imambfm  34264  totprobd  34428  dstrvprob  34474  ballotlem2  34491  requad2  47610  scmsuppss  48287  lincvalsc0  48338  linc0scn0  48340  lincdifsn  48341  linc1  48342  lincsum  48346  lincscm  48347  lcoss  48353  lincext3  48373  islindeps2  48400  itscnhlinecirc02p  48706
  Copyright terms: Public domain W3C validator