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

Theorem elelpwi 4004
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 4002 . . 3  |-  ( B  e.  ~P C  ->  B  C_  C )
21sseld 3485 . 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 1802   ~Pcpw 3993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472  df-pw 3995
This theorem is referenced by:  unipw  4683  axdc2lem  8826  axdc3lem4  8831  hash2sspr  12500  homarel  15232  bwthOLD  19777  txdis  19999  fpwrelmap  27421  insiga  28003  measinblem  28057  ddemeas  28074  imambfm  28099  totprobd  28231  dstrvprob  28276  ballotlem2  28293  scmsuppss  32675  lincvalsc0  32732  linc0scn0  32734  lincdifsn  32735  linc1  32736  lincsum  32740  lincscm  32741  lcoss  32747  lincext3  32767  islindeps2  32794
  Copyright terms: Public domain W3C validator