Theorem elpwid 4013

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

Syntax hints:   -> wi 4   e. wcel 1762   C_ wss 3469   ~Pcpw 4003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483  df-pw 4005

This theorem is referenced by:  fopwdom  7615  ssenen  7681  fival  7861  dffi2  7872  elfiun  7879  tskwe  8320  acndom2  8424  fodomfi2  8430  infpwfien  8432  dfac12lem2  8513  ackbij1lem9  8597  ackbij1lem10  8598  ackbij1lem11  8599  ackbij1lem16  8604  ackbij2lem3  8610  cfss  8634  fin23lem7  8685  fin23lem11  8686  enfin2i  8690  isf32lem8  8729  isf34lem4  8746  isf34lem7  8748  isf34lem6  8749  isfin1-3  8755  fin1a2lem13  8781  ttukeylem6  8883  uzssz  11090  elfzoelz  11786  ackbijnn  13592  incexclem  13600  smuval2  13980  smupvallem  13981  smueqlem  13988  ramub1lem1  14392  ramub1lem2  14393  restid2  14675  mress  14837  mrcuni  14865  mreexexlem4d  14891  mreexexd  14892  mreexdomd  14893  acsfn  14903  isdrs2  15415  ipodrsima  15641  isacs3lem  15642  acsfiindd  15653  lagsubg2  16050  cntzrcl  16153  sylow1lem2  16408  sylow1lem3  16409  sylow1lem4  16410  sylow2alem2  16427  sylow2a  16428  lsmpropd  16484  lssacs  17389  lssacsex  17566  lbsextlem2  17581  lbsextlem3  17582  lbsextlem4  17583  elocv  18459  ppttop  19267  epttop  19269  clsval2  19310  mretopd  19352  neiss2  19361  neiptopnei  19392  ordtbas  19452  subbascn  19514  discmp  19657  uncmp  19662  concompcon  19692  1stcfb  19705  2ndcdisj  19716  restnlly  19742  nllyrest  19746  nllyidm  19749  cldllycmp  19755  1stckgenlem  19782  dfac14  19847  xkoccn  19848  txnlly  19866  txkgen  19881  xkopt  19884  xkoco2cn  19887  xkoinjcn  19916  tgqtop  19941  nrmhmph  20023  fbelss  20062  fbssfi  20066  infil  20092  alexsubALTlem3  20277  alexsubALTlem4  20278  ustssxp  20435  trust  20460  utopsnneiplem  20478  blssm  20649  blin2  20660  metustssOLD  20784  metustss  20785  metustfbasOLD  20796  metustfbas  20797  metustOLD  20798  metust  20799  metutopOLD  20813  psmetutop  20814  restmetu  20818  icccmplem2  21056  cncfrss  21123  cncfrss2  21124  bndth  21186  lebnum  21192  ovolicc2  21661  vitalilem5  21749  i1fd  21816  dvbsss  22034  perfdvf  22035  plybss  22319  wilthlem2  23064  uhgrass  23969  umgrass  23982  usgrass  24024  eupath2  24642  ubthlem1  25448  ssnnssfz  27251  indf1ofs  27665  esumval  27683  esumel  27684  gsumesum  27693  esumlub  27694  esumpcvgval  27710  esumcvg  27718  elsigass  27751  br2base  27866  sxbrsigalem0  27868  dya2iocucvr  27881  sxbrsigalem2  27883  sxbrsiga  27887  eulerpartlemgvv  27941  coinfliplem  28043  ballotlemfmpn  28059  cvmliftmolem2  28353  cvmlift3lem8  28397  cnambfre  29627  neibastop1  29767  neibastop2lem  29768  neibastop2  29769  filnetlem4  29789  heiborlem3  29899  heiborlem5  29901  heiborlem6  29902  heiborlem10  29906  heibor  29907  elrfi  30217  elrfirn  30218  elrfirn2  30219  ismrcd1  30221  istopclsd  30223  mrefg3  30231  aomclem2  30594  lsmfgcl  30613  lmhmfgima  30623  elmnc  30679  stoweidlem39  31294  stoweidlem50  31305  ssnn0ssfz  31877  mapd1o  36320