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

Theorem elpwid 3710
Description: An element of a power class is a subclass. Deduction form of elpwi 3709. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elpwid.1  |-  ( ph  ->  A  e.  ~P B
)
Assertion
Ref Expression
elpwid  |-  ( ph  ->  A  C_  B )

Proof of Theorem elpwid
StepHypRef Expression
1 elpwid.1 . 2  |-  ( ph  ->  A  e.  ~P B
)
2 elpwi 3709 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
31, 2syl 15 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    C_ wss 3228   ~Pcpw 3701
This theorem is referenced by:  incexclem  12392  mreexexlem4d  13648  mreexexd  13649  mreexdomd  13650  acsfiindd  14379  lssacsex  15996  neiptopnei  23445  ustssxp  23510  trust  23533  utopsnneiplem  23551  metustss  23595  metustfbas  23601  metust  23602  metutop  23611  restmetu  23615  indf1ofs  23689  gsumesum  23717  esumlub  23718  br2base  23883  sxbrsigalem0  23885  dya2iocucvr  23898  sxbrsigalem2  23900  sxbrsiga  23904  uhgrass  27512  usgrass  27539
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242  df-pw 3703
  Copyright terms: Public domain W3C validator