Theorem elpwid 3680

Description: An element of a power class is a subclass. Deduction form of elpwi 3678. (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

Step	Hyp	Ref	Expression
1		elpwid.1	. 2 |- ( ph -> A e. ~P B )
2		elpwi 3678	. 2 |- ( A e. ~P B -> A C_ B )
3	1, 2	syl 14	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   e. wcel 2203   C_ wss 3211   ~Pcpw 3669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224  df-pw 3671

This theorem is referenced by:  fopwdom  7089  ssenen  7105  fival  7257  fiuni  7265  3nelsucpw1  7544  elnp1st2nd  7791  ixxssxr  10233  elfzoelz  10481  ballotfilem2  13142  restid2  13461  epttop  14955  neiss2  15007  blssm  15286  blin2  15297  cncfrss  15440  cncfrss2  15441  dvidsslem  15558  dvconstss  15563  plybss  15598  uhgrss  16070  upgrss  16094  upgr1een  16119  usgrss  16172  eupth2lemsfi  16473  pw1ndom3lem  16763  pwle2  16772