Theorem elpwid 4508

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  fopwdom  8608  ssenen  8675  fival  8860  dffi2  8871  elfiun  8878  tskwe  9363  acndom2  9465  fodomfi2  9471  infpwfien  9473  dfac12lem2  9555  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1lem11  9641  ackbij1lem16  9646  ackbij2lem3  9652  cfss  9676  fin23lem7  9727  fin23lem11  9728  enfin2i  9732  isf32lem8  9771  isf34lem4  9788  isf34lem7  9790  isf34lem6  9791  isfin1-3  9797  fin1a2lem13  9823  ttukeylem6  9925  uzssz  12252  elfzoelz  13033  ackbijnn  15175  incexclem  15183  smuval2  15821  smupvallem  15822  smueqlem  15829  ramub1lem1  16352  ramub1lem2  16353  restid2  16696  mress  16856  mrcuni  16884  mreexexlem4d  16910  mreexexd  16911  mreexdomd  16912  isacs2  16916  acsfn  16922  isdrs2  17541  ipodrsima  17767  isacs3lem  17768  acsfiindd  17779  lagsubg2  18333  cntzrcl  18449  sylow1lem2  18716  sylow1lem3  18717  sylow1lem4  18718  sylow2alem2  18735  sylow2a  18736  lsmpropd  18795  lssacs  19732  lssacsex  19909  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  elocv  20357  ppttop  21612  epttop  21614  clsval2  21655  mretopd  21697  neiss2  21706  neiptopnei  21737  ordtbas  21797  subbascn  21859  discmp  22003  uncmp  22008  conncompconn  22037  1stcfb  22050  2ndcdisj  22061  restnlly  22087  nllyrest  22091  nllyidm  22094  cldllycmp  22100  1stckgenlem  22158  dfac14  22223  xkoccn  22224  txnlly  22242  txkgen  22257  xkopt  22260  xkoco2cn  22263  xkoinjcn  22292  tgqtop  22317  nrmhmph  22399  fbelss  22438  fbssfi  22442  infil  22468  alexsubALTlem3  22654  alexsubALTlem4  22655  ustssxp  22810  trust  22835  utopsnneiplem  22853  blssm  23025  blin2  23036  metustss  23158  metust  23165  psmetutop  23174  restmetu  23177  icccmplem2  23428  cncfrss  23496  cncfrss2  23497  bndth  23563  lebnum  23569  ovolicc2  24126  vitalilem5  24216  i1fd  24285  dvbsss  24505  perfdvf  24506  plybss  24791  wilthlem2  25654  f1otrg  26665  uhgrss  26857  upgrss  26881  usgrss  26967  eupth2lems  28023  ubthlem1  28653  elpwdifcl  30299  elpwiuncl  30300  ssnnssfz  30536  pwrssmgc  30706  trsp2cyc  30815  zarcmplem  31234  indf1ofs  31395  esumval  31415  esumel  31416  gsumesum  31428  esumlub  31429  esumpcvgval  31447  esumcvg  31455  elsigass  31494  ispisys2  31522  sigapildsyslem  31530  sigapildsys  31531  ldgenpisyslem1  31532  ldgenpisys  31535  dynkin  31536  rossspw  31538  srossspw  31545  ddemeas  31605  br2base  31637  sxbrsigalem0  31639  dya2iocucvr  31652  sxbrsigalem2  31654  sxbrsiga  31658  oms0  31665  omssubadd  31668  carsguni  31676  elcarsgss  31677  carsggect  31686  omsmeas  31691  eulerpartlemgvv  31744  coinfliplem  31846  ballotlemfmpn  31862  cvmliftmolem2  32642  cvmlift3lem8  32686  neibastop1  33820  neibastop2lem  33821  neibastop2  33822  filnetlem4  33842  cnambfre  35105  heiborlem3  35251  heiborlem5  35253  heiborlem6  35254  heiborlem10  35258  heibor  35259  mapd1o  38944  elrfi  39635  elrfirn  39636  elrfirn2  39637  ismrcd1  39639  istopclsd  39641  mrefg3  39649  aomclem2  39999  lsmfgcl  40018  lmhmfgima  40028  elmnc  40080  rfovcnvf1od  40705  rfovcnvfvd  40708  fsovrfovd  40710  fsovcnvlem  40714  dssmapnvod  40721  ntrk0kbimka  40742  clsk3nimkb  40743  neik0pk1imk0  40750  ntrclsfveq1  40763  ntrclsfveq2  40764  ntrclsfveq  40765  ntrclsss  40766  ntrclsiso  40770  ntrclsk2  40771  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  ntrclsk4  40775  ntrneifv3  40785  ntrneineine0lem  40786  ntrneineine1lem  40787  ntrneifv4  40788  ntrneiel2  40789  ntrneicls00  40792  ntrneicls11  40793  ntrneiiso  40794  ntrneik2  40795  ntrneikb  40797  ntrneixb  40798  ntrneik3  40799  ntrneix3  40800  ntrneik13  40801  ntrneix13  40802  ntrneik4w  40803  clsneiel2  40812  clsneifv3  40813  clsneifv4  40814  neicvgel2  40823  neicvgfv  40824  gneispb  40834  elpwinss  41683  stoweidlem39  42681  stoweidlem50  42692  sge0resrnlem  43042  sge0iunmptlemre  43054  psmeasurelem  43109  psmeasure  43110  ssnn0ssfz  44751