Theorem elpwid 3961

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

Syntax hints:   -> wi 4   e. wcel 1887   C_ wss 3404   ~Pcpw 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953

This theorem is referenced by:  fopwdom  7680  ssenen  7746  fival  7926  dffi2  7937  elfiun  7944  tskwe  8384  acndom2  8485  fodomfi2  8491  infpwfien  8493  dfac12lem2  8574  ackbij1lem9  8658  ackbij1lem10  8659  ackbij1lem11  8660  ackbij1lem16  8665  ackbij2lem3  8671  cfss  8695  fin23lem7  8746  fin23lem11  8747  enfin2i  8751  isf32lem8  8790  isf34lem4  8807  isf34lem7  8809  isf34lem6  8810  isfin1-3  8816  fin1a2lem13  8842  ttukeylem6  8944  uzssz  11178  elfzoelz  11920  ackbijnn  13886  incexclem  13894  smuval2  14456  smupvallem  14457  smueqlem  14464  ramub1lem1  14984  ramub1lem2  14985  restid2  15329  mress  15499  mrcuni  15527  mreexexlem4d  15553  mreexexd  15554  mreexdomd  15555  acsfn  15565  isdrs2  16184  ipodrsima  16411  isacs3lem  16412  acsfiindd  16423  lagsubg2  16878  cntzrcl  16981  sylow1lem2  17251  sylow1lem3  17252  sylow1lem4  17253  sylow2alem2  17270  sylow2a  17271  lsmpropd  17327  lssacs  18190  lssacsex  18367  lbsextlem2  18382  lbsextlem3  18383  lbsextlem4  18384  elocv  19231  ppttop  20022  epttop  20024  clsval2  20065  mretopd  20108  neiss2  20117  neiptopnei  20148  ordtbas  20208  subbascn  20270  discmp  20413  uncmp  20418  concompcon  20447  1stcfb  20460  2ndcdisj  20471  restnlly  20497  nllyrest  20501  nllyidm  20504  cldllycmp  20510  1stckgenlem  20568  dfac14  20633  xkoccn  20634  txnlly  20652  txkgen  20667  xkopt  20670  xkoco2cn  20673  xkoinjcn  20702  tgqtop  20727  nrmhmph  20809  fbelss  20848  fbssfi  20852  infil  20878  alexsubALTlem3  21064  alexsubALTlem4  21065  ustssxp  21219  trust  21244  utopsnneiplem  21262  blssm  21433  blin2  21444  metustss  21566  metustfbas  21572  metust  21573  psmetutop  21582  restmetu  21585  icccmplem2  21841  cncfrss  21923  cncfrss2  21924  bndth  21986  lebnum  21995  ovolicc2  22476  vitalilem5  22570  i1fd  22639  dvbsss  22857  perfdvf  22858  plybss  23148  wilthlem2  23994  f1otrg  24901  uhgrass  25033  umgrass  25046  usgrass  25088  eupath2  25708  ubthlem1  26512  elpwdifcl  28155  elpwiuncl  28156  ssnnssfz  28367  indf1ofs  28847  esumval  28867  esumel  28868  gsumesum  28880  esumlub  28881  esumpcvgval  28899  esumcvg  28907  elsigass  28947  ispisys2  28975  sigapildsyslem  28983  sigapildsys  28984  ldgenpisys  28988  dynkin  28989  rossspw  28991  srossspw  28998  ddemeas  29059  br2base  29091  sxbrsigalem0  29093  dya2iocucvr  29106  sxbrsigalem2  29108  sxbrsiga  29112  oms0  29125  omssubadd  29128  omssubaddOLD  29132  carsguni  29140  elcarsgss  29141  carsggect  29150  omsmeas  29155  omsmeasOLD  29156  eulerpartlemgvv  29209  coinfliplem  29311  ballotlemfmpn  29327  cvmliftmolem2  30005  cvmlift3lem8  30049  neibastop1  31015  neibastop2lem  31016  neibastop2  31017  filnetlem4  31037  cnambfre  31989  heiborlem3  32145  heiborlem5  32147  heiborlem6  32148  heiborlem10  32152  heibor  32153  mapd1o  35216  elrfi  35536  elrfirn  35537  elrfirn2  35538  ismrcd1  35540  istopclsd  35542  mrefg3  35550  aomclem2  35913  lsmfgcl  35932  lmhmfgima  35942  elmnc  35995  stoweidlem39  37900  stoweidlem50  37911  sge0resrnlem  38245  sge0iunmptlemre  38257  psmeasurelem  38308  psmeasure  38309  uhgrss  39155  upgrss  39180  usgrss  39261  uhgssALTV  39734  ssnn0ssfz  40183