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

Theorem elelpwi 4510
 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 4507 . . 3 (𝐵 ∈ 𝒫 𝐶𝐵𝐶)
21sseld 3894 . 2 (𝐵 ∈ 𝒫 𝐶 → (𝐴𝐵𝐴𝐶))
32impcom 411 1 ((𝐴𝐵𝐵 ∈ 𝒫 𝐶) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  𝒫 cpw 4498 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3868  df-ss 3878  df-pw 4500 This theorem is referenced by:  unipw  5316  axdc2lem  9922  axdc3lem4  9927  homarel  17377  txdis  22347  uhgredgrnv  27037  fpwrelmap  30606  insiga  31638  measinblem  31721  ddemeas  31737  imambfm  31762  totprobd  31926  dstrvprob  31971  ballotlem2  31988  requad2  44568  scmsuppss  45201  lincvalsc0  45255  linc0scn0  45257  lincdifsn  45258  linc1  45259  lincsum  45263  lincscm  45264  lcoss  45270  lincext3  45290  islindeps2  45317  itscnhlinecirc02p  45624
 Copyright terms: Public domain W3C validator