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

Theorem elelpwi 3866
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 3864 . . 3  |-  ( B  e.  ~P C  ->  B  C_  C )
21sseld 3350 . 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 1756   ~Pcpw 3855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857
This theorem is referenced by:  unipw  4537  axdc2lem  8609  axdc3lem4  8614  homarel  14896  bwthOLD  18989  txdis  19180  fpwrelmap  25984  insiga  26532  measinblem  26586  ddemeas  26604  imambfm  26629  totprobd  26761  dstrvprob  26806  ballotlem2  26823  hash2sspr  30180  scmsuppss  30736  lincvalsc0  30844  linc0scn0  30846  lincdifsn  30847  linc1  30848  lincsum  30852  lincscm  30853  lcoss  30859  lincext3  30879  islindeps2  30906
  Copyright terms: Public domain W3C validator