Theorem elpwid 3858

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

Syntax hints:   -> wi 4   e. wcel 1755   C_ wss 3316   ~Pcpw 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850

This theorem is referenced by:  fopwdom  7407  ssenen  7473  fival  7650  dffi2  7661  elfiun  7668  tskwe  8108  acndom2  8212  fodomfi2  8218  infpwfien  8220  dfac12lem2  8301  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1lem11  8387  ackbij1lem16  8392  ackbij2lem3  8398  cfss  8422  fin23lem7  8473  fin23lem11  8474  enfin2i  8478  isf32lem8  8517  isf34lem4  8534  isf34lem7  8536  isf34lem6  8537  isfin1-3  8543  fin1a2lem13  8569  ttukeylem6  8671  uzssz  10868  elfzoelz  11537  ackbijnn  13274  incexclem  13282  smuval2  13661  smupvallem  13662  smueqlem  13669  ramub1lem1  14070  ramub1lem2  14071  restid2  14352  mress  14514  mrcuni  14542  mreexexlem4d  14568  mreexexd  14569  mreexdomd  14570  acsfn  14580  isdrs2  15092  ipodrsima  15318  isacs3lem  15319  acsfiindd  15330  lagsubg2  15722  cntzrcl  15825  sylow1lem2  16078  sylow1lem3  16079  sylow1lem4  16080  sylow2alem2  16097  sylow2a  16098  lsmpropd  16154  lssacs  16970  lssacsex  17147  lbsextlem2  17162  lbsextlem3  17163  lbsextlem4  17164  elocv  17935  ppttop  18453  epttop  18455  clsval2  18496  mretopd  18538  neiss2  18547  neiptopnei  18578  ordtbas  18638  subbascn  18700  discmp  18843  uncmp  18848  concompcon  18878  1stcfb  18891  2ndcdisj  18902  restnlly  18928  nllyrest  18932  nllyidm  18935  cldllycmp  18941  1stckgenlem  18968  dfac14  19033  xkoccn  19034  txnlly  19052  txkgen  19067  xkopt  19070  xkoco2cn  19073  xkoinjcn  19102  tgqtop  19127  nrmhmph  19209  fbelss  19248  fbssfi  19252  infil  19278  alexsubALTlem3  19463  alexsubALTlem4  19464  ustssxp  19621  trust  19646  utopsnneiplem  19664  blssm  19835  blin2  19846  metustssOLD  19970  metustss  19971  metustfbasOLD  19982  metustfbas  19983  metustOLD  19984  metust  19985  metutopOLD  19999  psmetutop  20000  restmetu  20004  icccmplem2  20242  cncfrss  20309  cncfrss2  20310  bndth  20372  lebnum  20378  ovolicc2  20847  vitalilem5  20934  i1fd  21001  dvbsss  21219  perfdvf  21220  plybss  21547  wilthlem2  22292  uhgrass  23063  umgrass  23076  usgrass  23106  eupath2  23424  ubthlem1  24094  ssnnssfz  25899  indf1ofs  26336  esumval  26354  esumel  26355  gsumesum  26364  esumlub  26365  esumpcvgval  26381  esumcvg  26389  elsigass  26422  br2base  26538  sxbrsigalem0  26540  dya2iocucvr  26553  sxbrsigalem2  26555  sxbrsiga  26559  eulerpartlemgvv  26607  coinfliplem  26709  ballotlemfmpn  26725  cvmliftmolem2  27019  cvmlift3lem8  27063  cnambfre  28284  neibastop1  28424  neibastop2lem  28425  neibastop2  28426  filnetlem4  28446  heiborlem3  28556  heiborlem5  28558  heiborlem6  28559  heiborlem10  28563  heibor  28564  elrfirn  28876  elrfirn2  28877  ismrcd1  28879  istopclsd  28881  mrefg3  28889  aomclem2  29253  lsmfgcl  29272  lmhmfgima  29282  elmnc  29338  stoweidlem39  29680  stoweidlem50  29691  mapd1o  34866