Theorem elpwid 3873

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

Syntax hints:   -> wi 4   e. wcel 1756   C_ wss 3331   ~Pcpw 3863

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 2423

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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338  df-ss 3345  df-pw 3865

This theorem is referenced by:  fopwdom  7422  ssenen  7488  fival  7665  dffi2  7676  elfiun  7683  tskwe  8123  acndom2  8227  fodomfi2  8233  infpwfien  8235  dfac12lem2  8316  ackbij1lem9  8400  ackbij1lem10  8401  ackbij1lem11  8402  ackbij1lem16  8407  ackbij2lem3  8413  cfss  8437  fin23lem7  8488  fin23lem11  8489  enfin2i  8493  isf32lem8  8532  isf34lem4  8549  isf34lem7  8551  isf34lem6  8552  isfin1-3  8558  fin1a2lem13  8584  ttukeylem6  8686  uzssz  10883  elfzoelz  11556  ackbijnn  13294  incexclem  13302  smuval2  13681  smupvallem  13682  smueqlem  13689  ramub1lem1  14090  ramub1lem2  14091  restid2  14372  mress  14534  mrcuni  14562  mreexexlem4d  14588  mreexexd  14589  mreexdomd  14590  acsfn  14600  isdrs2  15112  ipodrsima  15338  isacs3lem  15339  acsfiindd  15350  lagsubg2  15745  cntzrcl  15848  sylow1lem2  16101  sylow1lem3  16102  sylow1lem4  16103  sylow2alem2  16120  sylow2a  16121  lsmpropd  16177  lssacs  17051  lssacsex  17228  lbsextlem2  17243  lbsextlem3  17244  lbsextlem4  17245  elocv  18096  ppttop  18614  epttop  18616  clsval2  18657  mretopd  18699  neiss2  18708  neiptopnei  18739  ordtbas  18799  subbascn  18861  discmp  19004  uncmp  19009  concompcon  19039  1stcfb  19052  2ndcdisj  19063  restnlly  19089  nllyrest  19093  nllyidm  19096  cldllycmp  19102  1stckgenlem  19129  dfac14  19194  xkoccn  19195  txnlly  19213  txkgen  19228  xkopt  19231  xkoco2cn  19234  xkoinjcn  19263  tgqtop  19288  nrmhmph  19370  fbelss  19409  fbssfi  19413  infil  19439  alexsubALTlem3  19624  alexsubALTlem4  19625  ustssxp  19782  trust  19807  utopsnneiplem  19825  blssm  19996  blin2  20007  metustssOLD  20131  metustss  20132  metustfbasOLD  20143  metustfbas  20144  metustOLD  20145  metust  20146  metutopOLD  20160  psmetutop  20161  restmetu  20165  icccmplem2  20403  cncfrss  20470  cncfrss2  20471  bndth  20533  lebnum  20539  ovolicc2  21008  vitalilem5  21095  i1fd  21162  dvbsss  21380  perfdvf  21381  plybss  21665  wilthlem2  22410  uhgrass  23243  umgrass  23256  usgrass  23286  eupath2  23604  ubthlem1  24274  ssnnssfz  26079  indf1ofs  26485  esumval  26503  esumel  26504  gsumesum  26513  esumlub  26514  esumpcvgval  26530  esumcvg  26538  elsigass  26571  br2base  26687  sxbrsigalem0  26689  dya2iocucvr  26702  sxbrsigalem2  26704  sxbrsiga  26708  eulerpartlemgvv  26762  coinfliplem  26864  ballotlemfmpn  26880  cvmliftmolem2  27174  cvmlift3lem8  27218  cnambfre  28443  neibastop1  28583  neibastop2lem  28584  neibastop2  28585  filnetlem4  28605  heiborlem3  28715  heiborlem5  28717  heiborlem6  28718  heiborlem10  28722  heibor  28723  elrfi  29033  elrfirn  29034  elrfirn2  29035  ismrcd1  29037  istopclsd  29039  mrefg3  29047  aomclem2  29411  lsmfgcl  29430  lmhmfgima  29440  elmnc  29496  stoweidlem39  29837  stoweidlem50  29848  ssnn0ssfz  30744  mapd1o  35296