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

Theorem elelpwi 4014
Description: If  A belongs to a part of  C then  A belongs to  C. (Contributed by FL, 3-Aug-2009.)
Assertion
Ref Expression
elelpwi  |-  ( ( A  e.  B  /\  B  e.  ~P C
)  ->  A  e.  C )

Proof of Theorem elelpwi
StepHypRef Expression
1 elpwi 4012 . . 3  |-  ( B  e.  ~P C  ->  B  C_  C )
21sseld 3496 . 2  |-  ( B  e.  ~P C  -> 
( A  e.  B  ->  A  e.  C ) )
32impcom 430 1  |-  ( ( A  e.  B  /\  B  e.  ~P C
)  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   ~Pcpw 4003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483  df-pw 4005
This theorem is referenced by:  unipw  4690  axdc2lem  8817  axdc3lem4  8822  hash2sspr  12479  homarel  15210  bwthOLD  19670  txdis  19861  fpwrelmap  27078  insiga  27627  measinblem  27681  ddemeas  27698  imambfm  27723  totprobd  27855  dstrvprob  27900  ballotlem2  27917  scmsuppss  31913  lincvalsc0  31970  linc0scn0  31972  lincdifsn  31973  linc1  31974  lincsum  31978  lincscm  31979  lcoss  31985  lincext3  32005  islindeps2  32032
  Copyright terms: Public domain W3C validator