Theorem elpwid 4541

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  fopwdom  8820  ssenen  8887  fival  9101  dffi2  9112  elfiun  9119  tskwe  9639  acndom2  9741  fodomfi2  9747  infpwfien  9749  dfac12lem2  9831  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1lem11  9917  ackbij1lem16  9922  ackbij2lem3  9928  cfss  9952  fin23lem7  10003  fin23lem11  10004  enfin2i  10008  isf32lem8  10047  isf34lem4  10064  isf34lem7  10066  isf34lem6  10067  isfin1-3  10073  fin1a2lem13  10099  ttukeylem6  10201  uzssz  12532  elfzoelz  13316  ackbijnn  15468  incexclem  15476  smuval2  16117  smupvallem  16118  smueqlem  16125  ramub1lem1  16655  ramub1lem2  16656  restid2  17058  mress  17219  mrcuni  17247  mreexexlem4d  17273  mreexexd  17274  mreexdomd  17275  isacs2  17279  acsfn  17285  isdrs2  17939  ipodrsima  18174  isacs3lem  18175  acsfiindd  18186  lagsubg2  18732  cntzrcl  18848  sylow1lem2  19119  sylow1lem3  19120  sylow1lem4  19121  sylow2alem2  19138  sylow2a  19139  lsmpropd  19198  lssacs  20144  lssacsex  20321  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  elocv  20785  ppttop  22065  epttop  22067  clsval2  22109  mretopd  22151  neiss2  22160  neiptopnei  22191  ordtbas  22251  subbascn  22313  discmp  22457  uncmp  22462  conncompconn  22491  1stcfb  22504  2ndcdisj  22515  restnlly  22541  nllyrest  22545  nllyidm  22548  cldllycmp  22554  1stckgenlem  22612  dfac14  22677  xkoccn  22678  txnlly  22696  txkgen  22711  xkopt  22714  xkoco2cn  22717  xkoinjcn  22746  tgqtop  22771  nrmhmph  22853  fbelss  22892  fbssfi  22896  infil  22922  alexsubALTlem3  23108  alexsubALTlem4  23109  ustssxp  23264  trust  23289  utopsnneiplem  23307  blssm  23479  blin2  23490  metustss  23613  metust  23620  psmetutop  23629  restmetu  23632  icccmplem2  23892  cncfrss  23960  cncfrss2  23961  bndth  24027  lebnum  24033  ovolicc2  24591  vitalilem5  24681  i1fd  24750  dvbsss  24971  perfdvf  24972  plybss  25260  wilthlem2  26123  f1otrg  27136  uhgrss  27337  upgrss  27361  usgrss  27447  eupth2lems  28503  ubthlem1  29133  elpwdifcl  30776  elpwiuncl  30777  ssnnssfz  31010  pwrssmgc  31180  trsp2cyc  31292  zarcmplem  31733  indf1ofs  31894  esumval  31914  esumel  31915  gsumesum  31927  esumlub  31928  esumpcvgval  31946  esumcvg  31954  elsigass  31993  ispisys2  32021  sigapildsyslem  32029  sigapildsys  32030  ldgenpisyslem1  32031  ldgenpisys  32034  dynkin  32035  rossspw  32037  srossspw  32044  ddemeas  32104  br2base  32136  sxbrsigalem0  32138  dya2iocucvr  32151  sxbrsigalem2  32153  sxbrsiga  32157  oms0  32164  omssubadd  32167  carsguni  32175  elcarsgss  32176  carsggect  32185  omsmeas  32190  eulerpartlemgvv  32243  coinfliplem  32345  ballotlemfmpn  32361  cvmliftmolem2  33144  cvmlift3lem8  33188  oldf  33968  newf  33969  leftf  33976  rightf  33977  elmade  33978  ssltleft  33981  ssltright  33982  cofsslt  34015  coinitsslt  34016  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  filnetlem4  34497  cnambfre  35752  heiborlem3  35898  heiborlem5  35900  heiborlem6  35901  heiborlem10  35905  heibor  35906  mapd1o  39589  sticksstones3  40032  elrfi  40432  elrfirn  40433  elrfirn2  40434  ismrcd1  40436  istopclsd  40438  mrefg3  40446  aomclem2  40796  lsmfgcl  40815  lmhmfgima  40825  elmnc  40877  rfovcnvf1od  41501  rfovcnvfvd  41504  fsovrfovd  41506  fsovcnvlem  41510  dssmapnvod  41517  ntrk0kbimka  41538  clsk3nimkb  41539  neik0pk1imk0  41546  ntrclsfveq1  41559  ntrclsfveq2  41560  ntrclsfveq  41561  ntrclsss  41562  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrclsk4  41571  ntrneifv3  41581  ntrneineine0lem  41582  ntrneineine1lem  41583  ntrneifv4  41584  ntrneiel2  41585  ntrneicls00  41588  ntrneicls11  41589  ntrneiiso  41590  ntrneik2  41591  ntrneikb  41593  ntrneixb  41594  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  ntrneik4w  41599  clsneiel2  41608  clsneifv3  41609  clsneifv4  41610  neicvgel2  41619  neicvgfv  41620  gneispb  41630  elpwinss  42486  stoweidlem39  43470  stoweidlem50  43481  sge0resrnlem  43831  sge0iunmptlemre  43843  psmeasurelem  43898  psmeasure  43899  ssnn0ssfz  45573  iscnrm3rlem3  46124  iscnrm3rlem8  46129  iscnrm3llem1  46131  iscnrm3llem2  46132  iscnrm3l  46133