Theorem elpwid 3768

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

Syntax hints:   -> wi 4   e. wcel 1721   C_ wss 3280   ~Pcpw 3759

This theorem is referenced by:  fopwdom  7175  ssenen  7240  fival  7375  dffi2  7386  elfiun  7393  tskwe  7793  acndom2  7891  fodomfi2  7897  infpwfien  7899  dfac12lem2  7980  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem11  8066  ackbij1lem16  8071  ackbij2lem3  8077  cfss  8101  fin23lem7  8152  fin23lem11  8153  enfin2i  8157  isf32lem8  8196  isf34lem4  8213  isf34lem7  8215  isf34lem6  8216  isfin1-3  8222  fin1a2lem13  8248  ttukeylem6  8350  uzssz  10461  elfzoelz  11095  ackbijnn  12562  incexclem  12571  smuval2  12949  smupvallem  12950  smueqlem  12957  ramub1lem1  13349  ramub1lem2  13350  restid2  13613  mress  13773  mrcuni  13801  mreexexlem4d  13827  mreexexd  13828  mreexdomd  13829  acsfn  13839  isdrs2  14351  ipodrsima  14546  isacs3lem  14547  acsfiindd  14558  lagsubg2  14956  cntzrcl  15081  sylow1lem2  15188  sylow1lem3  15189  sylow1lem4  15190  sylow2alem2  15207  sylow2a  15208  lsmpropd  15264  lssacs  15998  lssacsex  16171  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  elocv  16850  ppttop  17026  epttop  17028  clsval2  17069  mretopd  17111  neiss2  17120  neiptopnei  17151  ordtbas  17210  subbascn  17272  discmp  17415  uncmp  17420  concompcon  17448  1stcfb  17461  2ndcdisj  17472  restnlly  17498  nllyrest  17502  nllyidm  17505  cldllycmp  17511  1stckgenlem  17538  dfac14  17603  xkoccn  17604  txnlly  17622  txkgen  17637  xkopt  17640  xkoco2cn  17643  xkoinjcn  17672  tgqtop  17697  nrmhmph  17779  fbelss  17818  fbssfi  17822  infil  17848  alexsubALTlem3  18033  alexsubALTlem4  18034  ustssxp  18187  trust  18212  utopsnneiplem  18230  blssm  18401  blin2  18412  metustssOLD  18536  metustss  18537  metustfbasOLD  18548  metustfbas  18549  metustOLD  18550  metust  18551  metutopOLD  18565  psmetutop  18566  restmetu  18570  icccmplem2  18807  cncfrss  18874  cncfrss2  18875  bndth  18936  lebnum  18942  ovolicc2  19371  vitalilem5  19457  i1fd  19526  dvbsss  19742  perfdvf  19743  plybss  20066  wilthlem2  20805  uhgrass  21294  umgrass  21307  usgrass  21337  eupath2  21655  ubthlem1  22325  ssnnssfz  24101  indf1ofs  24376  esumval  24394  esumel  24395  gsumesum  24404  esumlub  24405  esumpcvgval  24421  esumcvg  24429  elsigass  24461  br2base  24572  sxbrsigalem0  24574  dya2iocucvr  24587  sxbrsigalem2  24589  sxbrsiga  24593  coinfliplem  24689  ballotlemfmpn  24705  cvmliftmolem2  24922  cvmlift3lem8  24966  cnambfre  26154  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  filnetlem4  26300  heiborlem3  26412  heiborlem5  26414  heiborlem6  26415  heiborlem10  26419  heibor  26420  elrfirn  26639  elrfirn2  26640  ismrcd1  26642  istopclsd  26644  mrefg3  26652  aomclem2  27020  lsmfgcl  27040  lmhmfgima  27050  elmnc  27209  stoweidlem39  27655  stoweidlem50  27666  mapd1o  32131

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761