Theorem elpwid 4572

Description: An element of a power class is a subclass. Deduction form of elpwi 4570. (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 4570	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-pw 4565

This theorem is referenced by:  cofon1  8636  cofon2  8637  fopwdom  9049  ssenen  9115  fival  9363  dffi2  9374  elfiun  9381  tskwe  9903  acndom2  10007  fodomfi2  10013  infpwfien  10015  dfac12lem2  10098  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1lem11  10182  ackbij1lem16  10187  ackbij2lem3  10193  cfss  10218  fin23lem7  10269  fin23lem11  10270  enfin2i  10274  isf32lem8  10313  isf34lem4  10330  isf34lem7  10332  isf34lem6  10333  isfin1-3  10339  fin1a2lem13  10365  ttukeylem6  10467  uzssz  12814  elfzoelz  13620  ackbijnn  15794  incexclem  15802  smuval2  16452  smupvallem  16453  smueqlem  16460  ramub1lem1  16997  ramub1lem2  16998  restid2  17393  mress  17554  mrcuni  17582  mreexexlem4d  17608  mreexexd  17609  mreexdomd  17610  isacs2  17614  acsfn  17620  isdrs2  18267  ipodrsima  18500  isacs3lem  18501  acsfiindd  18512  lagsubg2  19126  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  cntzrcl  19259  sylow1lem2  19529  sylow1lem3  19530  sylow1lem4  19531  sylow2alem2  19548  sylow2a  19549  lsmpropd  19607  lssacs  20873  lssacsex  21054  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  rhmqusnsg  21195  elocv  21577  ppttop  22894  epttop  22896  clsval2  22937  mretopd  22979  neiss2  22988  neiptopnei  23019  ordtbas  23079  subbascn  23141  discmp  23285  uncmp  23290  conncompconn  23319  1stcfb  23332  2ndcdisj  23343  restnlly  23369  nllyrest  23373  nllyidm  23376  cldllycmp  23382  1stckgenlem  23440  dfac14  23505  xkoccn  23506  txnlly  23524  txkgen  23539  xkopt  23542  xkoco2cn  23545  xkoinjcn  23574  tgqtop  23599  nrmhmph  23681  fbelss  23720  fbssfi  23724  infil  23750  alexsubALTlem3  23936  alexsubALTlem4  23937  ustssxp  24092  trust  24117  utopsnneiplem  24135  blssm  24306  blin2  24317  metustss  24439  metust  24446  psmetutop  24455  restmetu  24458  icccmplem2  24712  cncfrss  24784  cncfrss2  24785  bndth  24857  lebnum  24863  ovolicc2  25423  vitalilem5  25513  i1fd  25582  dvbsss  25803  perfdvf  25804  plybss  26099  wilthlem2  26979  oldf  27765  newf  27766  leftf  27777  rightf  27778  elmade  27779  ssltleft  27782  ssltright  27783  cofsslt  27826  coinitsslt  27827  f1otrg  28798  uhgrss  28991  upgrss  29015  usgrss  29101  eupth2lems  30167  ubthlem1  30799  elpwdifcl  32455  elpwiuncl  32456  ssnnssfz  32710  indf1ofs  32789  pwrssmgc  32926  trsp2cyc  33080  lmhmqusker  33388  rhmquskerlem  33396  exsslsb  33592  zarcmplem  33871  esumval  34036  esumel  34037  gsumesum  34049  esumlub  34050  esumpcvgval  34068  esumcvg  34076  elsigass  34115  ispisys2  34143  sigapildsyslem  34151  sigapildsys  34152  ldgenpisyslem1  34153  ldgenpisys  34156  dynkin  34157  rossspw  34159  srossspw  34166  ddemeas  34226  br2base  34260  sxbrsigalem0  34262  dya2iocucvr  34275  sxbrsigalem2  34277  sxbrsiga  34281  oms0  34288  omssubadd  34291  carsguni  34299  elcarsgss  34300  carsggect  34309  omsmeas  34314  eulerpartlemgvv  34367  coinfliplem  34470  ballotlemfmpn  34486  cvmliftmolem2  35269  cvmlift3lem8  35313  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  filnetlem4  36369  cnambfre  37662  heiborlem3  37807  heiborlem5  37809  heiborlem6  37810  heiborlem10  37814  heibor  37815  mapd1o  41642  sticksstones3  42136  prjcrv0  42621  elrfi  42682  elrfirn  42683  elrfirn2  42684  ismrcd1  42686  istopclsd  42688  mrefg3  42696  aomclem2  43044  lsmfgcl  43063  lmhmfgima  43073  elmnc  43125  fpwfvss  43401  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  ntrk0kbimka  44028  clsk3nimkb  44029  neik0pk1imk0  44036  ntrclsfveq1  44049  ntrclsfveq2  44050  ntrclsfveq  44051  ntrclsss  44052  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneifv3  44071  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneifv4  44074  ntrneiel2  44075  ntrneicls00  44078  ntrneicls11  44079  ntrneiiso  44080  ntrneik2  44081  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  clsneiel2  44098  clsneifv3  44099  clsneifv4  44100  neicvgel2  44109  neicvgfv  44110  gneispb  44120  elpwinss  45043  stoweidlem39  46037  stoweidlem50  46048  sge0resrnlem  46401  sge0iunmptlemre  46413  psmeasurelem  46468  psmeasure  46469  isubgrvtxuhgr  47864  isuspgrim0  47894  isuspgrimlem  47895  uhgrimisgrgriclem  47930  ssnn0ssfz  48337  iscnrm3rlem3  48930  iscnrm3rlem8  48935  iscnrm3llem1  48937  iscnrm3llem2  48938  iscnrm3l  48939  pgindlem  49704