Theorem elpwid 4009

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

Syntax hints:   -> wi 4   e. wcel 1823   C_ wss 3461   ~Pcpw 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  fopwdom  7618  ssenen  7684  fival  7864  dffi2  7875  elfiun  7882  tskwe  8322  acndom2  8426  fodomfi2  8432  infpwfien  8434  dfac12lem2  8515  ackbij1lem9  8599  ackbij1lem10  8600  ackbij1lem11  8601  ackbij1lem16  8606  ackbij2lem3  8612  cfss  8636  fin23lem7  8687  fin23lem11  8688  enfin2i  8692  isf32lem8  8731  isf34lem4  8748  isf34lem7  8750  isf34lem6  8751  isfin1-3  8757  fin1a2lem13  8783  ttukeylem6  8885  uzssz  11101  elfzoelz  11804  ackbijnn  13722  incexclem  13730  smuval2  14216  smupvallem  14217  smueqlem  14224  ramub1lem1  14628  ramub1lem2  14629  restid2  14920  mress  15082  mrcuni  15110  mreexexlem4d  15136  mreexexd  15137  mreexdomd  15138  acsfn  15148  isdrs2  15767  ipodrsima  15994  isacs3lem  15995  acsfiindd  16006  lagsubg2  16461  cntzrcl  16564  sylow1lem2  16818  sylow1lem3  16819  sylow1lem4  16820  sylow2alem2  16837  sylow2a  16838  lsmpropd  16894  lssacs  17808  lssacsex  17985  lbsextlem2  18000  lbsextlem3  18001  lbsextlem4  18002  elocv  18872  ppttop  19675  epttop  19677  clsval2  19718  mretopd  19760  neiss2  19769  neiptopnei  19800  ordtbas  19860  subbascn  19922  discmp  20065  uncmp  20070  concompcon  20099  1stcfb  20112  2ndcdisj  20123  restnlly  20149  nllyrest  20153  nllyidm  20156  cldllycmp  20162  1stckgenlem  20220  dfac14  20285  xkoccn  20286  txnlly  20304  txkgen  20319  xkopt  20322  xkoco2cn  20325  xkoinjcn  20354  tgqtop  20379  nrmhmph  20461  fbelss  20500  fbssfi  20504  infil  20530  alexsubALTlem3  20715  alexsubALTlem4  20716  ustssxp  20873  trust  20898  utopsnneiplem  20916  blssm  21087  blin2  21098  metustssOLD  21222  metustss  21223  metustfbasOLD  21234  metustfbas  21235  metustOLD  21236  metust  21237  metutopOLD  21251  psmetutop  21252  restmetu  21256  icccmplem2  21494  cncfrss  21561  cncfrss2  21562  bndth  21624  lebnum  21630  ovolicc2  22099  vitalilem5  22187  i1fd  22254  dvbsss  22472  perfdvf  22473  plybss  22757  wilthlem2  23541  f1otrg  24376  uhgrass  24508  umgrass  24521  usgrass  24563  eupath2  25182  ubthlem1  25984  elpwdifcl  27621  elpwiuncl  27622  ssnnssfz  27831  indf1ofs  28255  esumval  28275  esumel  28276  gsumesum  28288  esumlub  28289  esumpcvgval  28307  esumcvg  28315  elsigass  28355  ispisys2  28383  sigapildsyslem  28387  sigapildsys  28388  ddemeas  28445  br2base  28477  sxbrsigalem0  28479  dya2iocucvr  28492  sxbrsigalem2  28494  sxbrsiga  28498  omssubadd  28508  carsguni  28516  elcarsgss  28517  carsggect  28526  omsmeas  28531  eulerpartlemgvv  28579  coinfliplem  28681  ballotlemfmpn  28697  cvmliftmolem2  28991  cvmlift3lem8  29035  cnambfre  30303  neibastop1  30417  neibastop2lem  30418  neibastop2  30419  filnetlem4  30439  heiborlem3  30549  heiborlem5  30551  heiborlem6  30552  heiborlem10  30556  heibor  30557  elrfi  30866  elrfirn  30867  elrfirn2  30868  ismrcd1  30870  istopclsd  30872  mrefg3  30880  aomclem2  31240  lsmfgcl  31259  lmhmfgima  31269  elmnc  31326  stoweidlem39  32060  stoweidlem50  32071  uhgss  32741  ssnn0ssfz  33192  mapd1o  37772