Theorem elpwid 4565

Description: An element of a power class is a subclass. Deduction form of elpwi 4563. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
elpwid.1	⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Assertion

Ref	Expression
elpwid	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwid

Step	Hyp	Ref	Expression
1		elpwid.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)
2		elpwi 4563	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-pw 4558

This theorem is referenced by:  cofon1  8610  cofon2  8611  fopwdom  9025  ssenen  9091  fival  9327  dffi2  9338  elfiun  9345  tskwe  9874  acndom2  9976  fodomfi2  9982  infpwfien  9984  dfac12lem2  10067  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem11  10151  ackbij1lem16  10156  ackbij2lem3  10162  cfss  10187  fin23lem7  10238  fin23lem11  10239  enfin2i  10243  isf32lem8  10282  isf34lem4  10299  isf34lem7  10301  isf34lem6  10302  isfin1-3  10308  fin1a2lem13  10334  ttukeylem6  10436  uzssz  12784  elfzoelz  13587  ackbijnn  15763  incexclem  15771  smuval2  16421  smupvallem  16422  smueqlem  16429  ramub1lem1  16966  ramub1lem2  16967  restid2  17362  mress  17524  mrcuni  17556  mreexexlem4d  17582  mreexexd  17583  mreexdomd  17584  isacs2  17588  acsfn  17594  isdrs2  18241  ipodrsima  18476  isacs3lem  18477  acsfiindd  18488  lagsubg2  19135  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  cntzrcl  19268  sylow1lem2  19540  sylow1lem3  19541  sylow1lem4  19542  sylow2alem2  19559  sylow2a  19560  lsmpropd  19618  lssacs  20930  lssacsex  21111  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  rhmqusnsg  21252  elocv  21635  ppttop  22963  epttop  22965  clsval2  23006  mretopd  23048  neiss2  23057  neiptopnei  23088  ordtbas  23148  subbascn  23210  discmp  23354  uncmp  23359  conncompconn  23388  1stcfb  23401  2ndcdisj  23412  restnlly  23438  nllyrest  23442  nllyidm  23445  cldllycmp  23451  1stckgenlem  23509  dfac14  23574  xkoccn  23575  txnlly  23593  txkgen  23608  xkopt  23611  xkoco2cn  23614  xkoinjcn  23643  tgqtop  23668  nrmhmph  23750  fbelss  23789  fbssfi  23793  infil  23819  alexsubALTlem3  24005  alexsubALTlem4  24006  ustssxp  24161  trust  24185  utopsnneiplem  24203  blssm  24374  blin2  24385  metustss  24507  metust  24514  psmetutop  24523  restmetu  24526  icccmplem2  24780  cncfrss  24852  cncfrss2  24853  bndth  24925  lebnum  24931  ovolicc2  25491  vitalilem5  25581  i1fd  25650  dvbsss  25871  perfdvf  25872  plybss  26167  wilthlem2  27047  oldf  27845  newf  27846  leftf  27863  rightf  27864  elmade  27865  sltsleft  27868  sltsright  27869  cofslts  27926  coinitslts  27927  f1otrg  28955  uhgrss  29149  upgrss  29173  usgrss  29259  eupth2lems  30325  ubthlem1  30957  elpwdifcl  32612  elpwiuncl  32613  ssnnssfz  32877  indf1ofs  32958  pwrssmgc  33092  trsp2cyc  33216  lmhmqusker  33509  rhmquskerlem  33517  esplylem  33742  esplymhp  33744  esplyfv1  33745  esplyfv  33746  esplyfval3  33748  exsslsb  33773  zarcmplem  34058  esumval  34223  esumel  34224  gsumesum  34236  esumlub  34237  esumpcvgval  34255  esumcvg  34263  elsigass  34302  ispisys2  34330  sigapildsyslem  34338  sigapildsys  34339  ldgenpisyslem1  34340  ldgenpisys  34343  dynkin  34344  rossspw  34346  srossspw  34353  ddemeas  34413  br2base  34446  sxbrsigalem0  34448  dya2iocucvr  34461  sxbrsigalem2  34463  sxbrsiga  34467  oms0  34474  omssubadd  34477  carsguni  34485  elcarsgss  34486  carsggect  34495  omsmeas  34500  eulerpartlemgvv  34553  coinfliplem  34656  ballotlemfmpn  34672  cvmliftmolem2  35495  cvmlift3lem8  35539  neibastop1  36572  neibastop2lem  36573  neibastop2  36574  filnetlem4  36594  cnambfre  37908  heiborlem3  38053  heiborlem5  38055  heiborlem6  38056  heiborlem10  38060  heibor  38061  mapd1o  42013  sticksstones3  42507  prjcrv0  42980  elrfi  43040  elrfirn  43041  elrfirn2  43042  ismrcd1  43044  istopclsd  43046  mrefg3  43054  aomclem2  43401  lsmfgcl  43420  lmhmfgima  43430  elmnc  43482  fpwfvss  43757  rfovcnvf1od  44349  rfovcnvfvd  44352  fsovrfovd  44354  fsovcnvlem  44358  dssmapnvod  44365  ntrk0kbimka  44384  clsk3nimkb  44385  neik0pk1imk0  44392  ntrclsfveq1  44405  ntrclsfveq2  44406  ntrclsfveq  44407  ntrclsss  44408  ntrclsiso  44412  ntrclsk2  44413  ntrclskb  44414  ntrclsk3  44415  ntrclsk13  44416  ntrclsk4  44417  ntrneifv3  44427  ntrneineine0lem  44428  ntrneineine1lem  44429  ntrneifv4  44430  ntrneiel2  44431  ntrneicls00  44434  ntrneicls11  44435  ntrneiiso  44436  ntrneik2  44437  ntrneikb  44439  ntrneixb  44440  ntrneik3  44441  ntrneix3  44442  ntrneik13  44443  ntrneix13  44444  ntrneik4w  44445  clsneiel2  44454  clsneifv3  44455  clsneifv4  44456  neicvgel2  44465  neicvgfv  44466  gneispb  44476  elpwinss  45398  stoweidlem39  46386  stoweidlem50  46397  sge0resrnlem  46750  sge0iunmptlemre  46762  psmeasurelem  46817  psmeasure  46818  isubgrvtxuhgr  48213  isuspgrim0  48243  isuspgrimlem  48244  uhgrimisgrgriclem  48279  ssnn0ssfz  48698  iscnrm3rlem3  49290  iscnrm3rlem8  49295  iscnrm3llem1  49297  iscnrm3llem2  49298  iscnrm3l  49299  pgindlem  50063