Theorem elpwid 3696

Description: An element of a power class is a subclass. Deduction form of elpwi 3694. (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 3694	. 2 |- ( A e. ~P B -> A C_ B )
3	1, 2	syl 14	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   e. wcel 2209   C_ wss 3220   ~Pcpw 3685

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-pw 3687

This theorem is referenced by:  fopwdom  7126  ssenen  7142  fival  7294  fiuni  7302  3nelsucpw1  7583  elnp1st2nd  7833  ixxssxr  10281  elfzoelz  10532  ballotfilem2  13206  ballotfilemfmpn  13212  restid2  13579  epttop  15114  neiss2  15166  blssm  15445  blin2  15456  cncfrss  15599  cncfrss2  15600  dvidsslem  15717  dvconstss  15722  plybss  15757  uhgrss  16230  upgrss  16254  upgr1een  16279  usgrss  16332  eupth2lemsfi  16633  pw1ndom3lem  16933  pwle2  16942