Theorem elpwid 4551

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

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 3907  df-pw 4544

This theorem is referenced by:  cofon1  8608  cofon2  8609  fopwdom  9023  ssenen  9089  fival  9325  dffi2  9336  elfiun  9343  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  12809  elfzoelz  13613  ackbijnn  15793  incexclem  15801  smuval2  16451  smupvallem  16452  smueqlem  16459  ramub1lem1  16997  ramub1lem2  16998  restid2  17393  mress  17555  mrcuni  17587  mreexexlem4d  17613  mreexexd  17614  mreexdomd  17615  isacs2  17619  acsfn  17625  isdrs2  18272  ipodrsima  18507  isacs3lem  18508  acsfiindd  18519  lagsubg2  19169  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  cntzrcl  19302  sylow1lem2  19574  sylow1lem3  19575  sylow1lem4  19576  sylow2alem2  19593  sylow2a  19594  lsmpropd  19652  lssacs  20962  lssacsex  21142  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  rhmqusnsg  21283  elocv  21648  ppttop  22972  epttop  22974  clsval2  23015  mretopd  23057  neiss2  23066  neiptopnei  23097  ordtbas  23157  subbascn  23219  discmp  23363  uncmp  23368  conncompconn  23397  1stcfb  23410  2ndcdisj  23421  restnlly  23447  nllyrest  23451  nllyidm  23454  cldllycmp  23460  1stckgenlem  23518  dfac14  23583  xkoccn  23584  txnlly  23602  txkgen  23617  xkopt  23620  xkoco2cn  23623  xkoinjcn  23652  tgqtop  23677  nrmhmph  23759  fbelss  23798  fbssfi  23802  infil  23828  alexsubALTlem3  24014  alexsubALTlem4  24015  ustssxp  24170  trust  24194  utopsnneiplem  24212  blssm  24383  blin2  24394  metustss  24516  metust  24523  psmetutop  24532  restmetu  24535  icccmplem2  24789  cncfrss  24858  cncfrss2  24859  bndth  24925  lebnum  24931  ovolicc2  25489  vitalilem5  25579  i1fd  25648  dvbsss  25869  perfdvf  25870  plybss  26159  wilthlem2  27032  oldf  27829  newf  27830  leftf  27847  rightf  27848  elmade  27849  sltsleft  27852  sltsright  27853  cofslts  27910  coinitslts  27911  f1otrg  28939  uhgrss  29133  upgrss  29157  usgrss  29243  eupth2lems  30308  ubthlem1  30941  elpwdifcl  32596  elpwiuncl  32597  ssnnssfz  32860  indf1ofs  32926  pwrssmgc  33060  trsp2cyc  33184  lmhmqusker  33477  rhmquskerlem  33485  esplylem  33710  esplymhp  33712  esplyfv1  33713  esplyfv  33714  esplyfval3  33716  exsslsb  33741  zarcmplem  34025  esumval  34190  esumel  34191  gsumesum  34203  esumlub  34204  esumpcvgval  34222  esumcvg  34230  elsigass  34269  ispisys2  34297  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  ldgenpisys  34310  dynkin  34311  rossspw  34313  srossspw  34320  ddemeas  34380  br2base  34413  sxbrsigalem0  34415  dya2iocucvr  34428  sxbrsigalem2  34430  sxbrsiga  34434  oms0  34441  omssubadd  34444  carsguni  34452  elcarsgss  34453  carsggect  34462  omsmeas  34467  eulerpartlemgvv  34520  coinfliplem  34623  ballotlemfmpn  34639  cvmliftmolem2  35464  cvmlift3lem8  35508  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  filnetlem4  36563  cnambfre  37989  heiborlem3  38134  heiborlem5  38136  heiborlem6  38137  heiborlem10  38141  heibor  38142  mapd1o  42094  sticksstones3  42587  prjcrv0  43066  elrfi  43126  elrfirn  43127  elrfirn2  43128  ismrcd1  43130  istopclsd  43132  mrefg3  43140  aomclem2  43483  lsmfgcl  43502  lmhmfgima  43512  elmnc  43564  fpwfvss  43839  rfovcnvf1od  44431  rfovcnvfvd  44434  fsovrfovd  44436  fsovcnvlem  44440  dssmapnvod  44447  ntrk0kbimka  44466  clsk3nimkb  44467  neik0pk1imk0  44474  ntrclsfveq1  44487  ntrclsfveq2  44488  ntrclsfveq  44489  ntrclsss  44490  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrclsk4  44499  ntrneifv3  44509  ntrneineine0lem  44510  ntrneineine1lem  44511  ntrneifv4  44512  ntrneiel2  44513  ntrneicls00  44516  ntrneicls11  44517  ntrneiiso  44518  ntrneik2  44519  ntrneikb  44521  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  ntrneik4w  44527  clsneiel2  44536  clsneifv3  44537  clsneifv4  44538  neicvgel2  44547  neicvgfv  44548  gneispb  44558  elpwinss  45480  stoweidlem39  46467  stoweidlem50  46478  sge0resrnlem  46831  sge0iunmptlemre  46843  psmeasurelem  46898  psmeasure  46899  isubgrvtxuhgr  48334  isuspgrim0  48364  isuspgrimlem  48365  uhgrimisgrgriclem  48400  ssnn0ssfz  48819  iscnrm3rlem3  49411  iscnrm3rlem8  49416  iscnrm3llem1  49418  iscnrm3llem2  49419  iscnrm3l  49420  pgindlem  50184