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

Theorem elelpwi 3972
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 3970 . . 3  |-  ( B  e.  ~P C  ->  B  C_  C )
21sseld 3456 . 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 1758   ~Pcpw 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436  df-ss 3443  df-pw 3963
This theorem is referenced by:  unipw  4643  axdc2lem  8721  axdc3lem4  8726  homarel  15015  bwthOLD  19139  txdis  19330  fpwrelmap  26177  insiga  26718  measinblem  26772  ddemeas  26789  imambfm  26814  totprobd  26946  dstrvprob  26991  ballotlem2  27008  hash2sspr  30368  scmsuppss  30926  lincvalsc0  31065  linc0scn0  31067  lincdifsn  31068  linc1  31069  lincsum  31073  lincscm  31074  lcoss  31080  lincext3  31100  islindeps2  31127
  Copyright terms: Public domain W3C validator