Theorem elpwid 4007

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

Syntax hints:   -> wi 4   e. wcel 1804   C_ wss 3461   ~Pcpw 3997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475  df-pw 3999

This theorem is referenced by:  fopwdom  7627  ssenen  7693  fival  7874  dffi2  7885  elfiun  7892  tskwe  8334  acndom2  8438  fodomfi2  8444  infpwfien  8446  dfac12lem2  8527  ackbij1lem9  8611  ackbij1lem10  8612  ackbij1lem11  8613  ackbij1lem16  8618  ackbij2lem3  8624  cfss  8648  fin23lem7  8699  fin23lem11  8700  enfin2i  8704  isf32lem8  8743  isf34lem4  8760  isf34lem7  8762  isf34lem6  8763  isfin1-3  8769  fin1a2lem13  8795  ttukeylem6  8897  uzssz  11109  elfzoelz  11808  ackbijnn  13619  incexclem  13627  smuval2  14009  smupvallem  14010  smueqlem  14017  ramub1lem1  14421  ramub1lem2  14422  restid2  14705  mress  14867  mrcuni  14895  mreexexlem4d  14921  mreexexd  14922  mreexdomd  14923  acsfn  14933  isdrs2  15442  ipodrsima  15669  isacs3lem  15670  acsfiindd  15681  lagsubg2  16136  cntzrcl  16239  sylow1lem2  16493  sylow1lem3  16494  sylow1lem4  16495  sylow2alem2  16512  sylow2a  16513  lsmpropd  16569  lssacs  17487  lssacsex  17664  lbsextlem2  17679  lbsextlem3  17680  lbsextlem4  17681  elocv  18572  ppttop  19381  epttop  19383  clsval2  19424  mretopd  19466  neiss2  19475  neiptopnei  19506  ordtbas  19566  subbascn  19628  discmp  19771  uncmp  19776  concompcon  19806  1stcfb  19819  2ndcdisj  19830  restnlly  19856  nllyrest  19860  nllyidm  19863  cldllycmp  19869  1stckgenlem  19927  dfac14  19992  xkoccn  19993  txnlly  20011  txkgen  20026  xkopt  20029  xkoco2cn  20032  xkoinjcn  20061  tgqtop  20086  nrmhmph  20168  fbelss  20207  fbssfi  20211  infil  20237  alexsubALTlem3  20422  alexsubALTlem4  20423  ustssxp  20580  trust  20605  utopsnneiplem  20623  blssm  20794  blin2  20805  metustssOLD  20929  metustss  20930  metustfbasOLD  20941  metustfbas  20942  metustOLD  20943  metust  20944  metutopOLD  20958  psmetutop  20959  restmetu  20963  icccmplem2  21201  cncfrss  21268  cncfrss2  21269  bndth  21331  lebnum  21337  ovolicc2  21806  vitalilem5  21894  i1fd  21961  dvbsss  22179  perfdvf  22180  plybss  22464  wilthlem2  23215  f1otrg  24046  uhgrass  24178  umgrass  24191  usgrass  24233  eupath2  24852  ubthlem1  25658  ssnnssfz  27469  indf1ofs  27912  esumval  27930  esumel  27931  gsumesum  27940  esumlub  27941  esumpcvgval  27957  esumcvg  27965  elsigass  27998  ddemeas  28081  br2base  28113  sxbrsigalem0  28115  dya2iocucvr  28128  sxbrsigalem2  28130  sxbrsiga  28134  oms0  28139  omsmon  28140  eulerpartlemgvv  28188  coinfliplem  28290  ballotlemfmpn  28306  cvmliftmolem2  28600  cvmlift3lem8  28644  cnambfre  30038  neibastop1  30152  neibastop2lem  30153  neibastop2  30154  filnetlem4  30174  heiborlem3  30284  heiborlem5  30286  heiborlem6  30287  heiborlem10  30291  heibor  30292  elrfi  30601  elrfirn  30602  elrfirn2  30603  ismrcd1  30605  istopclsd  30607  mrefg3  30615  aomclem2  30976  lsmfgcl  30995  lmhmfgima  31005  elmnc  31061  stoweidlem39  31710  stoweidlem50  31721  uhgss  32207  ssnn0ssfz  32666  mapd1o  37109