Theorem elpwid 4574

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3913  𝒫 cpw 4565

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  cofon1  8623  cofon2  8624  fopwdom  9031  ssenen  9102  fival  9357  dffi2  9368  elfiun  9375  tskwe  9895  acndom2  9999  fodomfi2  10005  infpwfien  10007  dfac12lem2  10089  ackbij1lem9  10173  ackbij1lem10  10174  ackbij1lem11  10175  ackbij1lem16  10180  ackbij2lem3  10186  cfss  10210  fin23lem7  10261  fin23lem11  10262  enfin2i  10266  isf32lem8  10305  isf34lem4  10322  isf34lem7  10324  isf34lem6  10325  isfin1-3  10331  fin1a2lem13  10357  ttukeylem6  10459  uzssz  12793  elfzoelz  13582  ackbijnn  15724  incexclem  15732  smuval2  16373  smupvallem  16374  smueqlem  16381  ramub1lem1  16909  ramub1lem2  16910  restid2  17326  mress  17487  mrcuni  17515  mreexexlem4d  17541  mreexexd  17542  mreexdomd  17543  isacs2  17547  acsfn  17553  isdrs2  18209  ipodrsima  18444  isacs3lem  18445  acsfiindd  18456  lagsubg2  19005  cntzrcl  19121  sylow1lem2  19395  sylow1lem3  19396  sylow1lem4  19397  sylow2alem2  19414  sylow2a  19415  lsmpropd  19473  lssacs  20485  lssacsex  20664  lbsextlem2  20679  lbsextlem3  20680  lbsextlem4  20681  elocv  21109  ppttop  22394  epttop  22396  clsval2  22438  mretopd  22480  neiss2  22489  neiptopnei  22520  ordtbas  22580  subbascn  22642  discmp  22786  uncmp  22791  conncompconn  22820  1stcfb  22833  2ndcdisj  22844  restnlly  22870  nllyrest  22874  nllyidm  22877  cldllycmp  22883  1stckgenlem  22941  dfac14  23006  xkoccn  23007  txnlly  23025  txkgen  23040  xkopt  23043  xkoco2cn  23046  xkoinjcn  23075  tgqtop  23100  nrmhmph  23182  fbelss  23221  fbssfi  23225  infil  23251  alexsubALTlem3  23437  alexsubALTlem4  23438  ustssxp  23593  trust  23618  utopsnneiplem  23636  blssm  23808  blin2  23819  metustss  23944  metust  23951  psmetutop  23960  restmetu  23963  icccmplem2  24223  cncfrss  24291  cncfrss2  24292  bndth  24358  lebnum  24364  ovolicc2  24923  vitalilem5  25013  i1fd  25082  dvbsss  25303  perfdvf  25304  plybss  25592  wilthlem2  26455  oldf  27230  newf  27231  leftf  27238  rightf  27239  elmade  27240  ssltleft  27243  ssltright  27244  cofsslt  27280  coinitsslt  27281  f1otrg  27876  uhgrss  28078  upgrss  28102  usgrss  28188  eupth2lems  29245  ubthlem1  29875  elpwdifcl  31518  elpwiuncl  31519  ssnnssfz  31758  pwrssmgc  31930  trsp2cyc  32042  ghmqusker  32272  lmhmqusker  32273  rhmqusker  32278  zarcmplem  32551  indf1ofs  32714  esumval  32734  esumel  32735  gsumesum  32747  esumlub  32748  esumpcvgval  32766  esumcvg  32774  elsigass  32813  ispisys2  32841  sigapildsyslem  32849  sigapildsys  32850  ldgenpisyslem1  32851  ldgenpisys  32854  dynkin  32855  rossspw  32857  srossspw  32864  ddemeas  32924  br2base  32958  sxbrsigalem0  32960  dya2iocucvr  32973  sxbrsigalem2  32975  sxbrsiga  32979  oms0  32986  omssubadd  32989  carsguni  32997  elcarsgss  32998  carsggect  33007  omsmeas  33012  eulerpartlemgvv  33065  coinfliplem  33167  ballotlemfmpn  33183  cvmliftmolem2  33963  cvmlift3lem8  34007  neibastop1  34907  neibastop2lem  34908  neibastop2  34909  filnetlem4  34929  cnambfre  36199  heiborlem3  36345  heiborlem5  36347  heiborlem6  36348  heiborlem10  36352  heibor  36353  mapd1o  40184  sticksstones3  40629  prjcrv0  41029  elrfi  41075  elrfirn  41076  elrfirn2  41077  ismrcd1  41079  istopclsd  41081  mrefg3  41089  aomclem2  41440  lsmfgcl  41459  lmhmfgima  41469  elmnc  41521  fpwfvss  41806  rfovcnvf1od  42398  rfovcnvfvd  42401  fsovrfovd  42403  fsovcnvlem  42407  dssmapnvod  42414  ntrk0kbimka  42433  clsk3nimkb  42434  neik0pk1imk0  42441  ntrclsfveq1  42454  ntrclsfveq2  42455  ntrclsfveq  42456  ntrclsss  42457  ntrclsiso  42461  ntrclsk2  42462  ntrclskb  42463  ntrclsk3  42464  ntrclsk13  42465  ntrclsk4  42466  ntrneifv3  42476  ntrneineine0lem  42477  ntrneineine1lem  42478  ntrneifv4  42479  ntrneiel2  42480  ntrneicls00  42483  ntrneicls11  42484  ntrneiiso  42485  ntrneik2  42486  ntrneikb  42488  ntrneixb  42489  ntrneik3  42490  ntrneix3  42491  ntrneik13  42492  ntrneix13  42493  ntrneik4w  42494  clsneiel2  42503  clsneifv3  42504  clsneifv4  42505  neicvgel2  42514  neicvgfv  42515  gneispb  42525  elpwinss  43379  stoweidlem39  44400  stoweidlem50  44411  sge0resrnlem  44764  sge0iunmptlemre  44776  psmeasurelem  44831  psmeasure  44832  ssnn0ssfz  46545  iscnrm3rlem3  47095  iscnrm3rlem8  47100  iscnrm3llem1  47102  iscnrm3llem2  47103  iscnrm3l  47104  pgindlem  47280