Theorem elpwid 4374

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

Syntax hints:   → wi 4   ∈ wcel 2157   ⊆ wss 3780  𝒫 cpw 4362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787  df-ss 3794  df-pw 4364

This theorem is referenced by:  fopwdom  8314  ssenen  8380  fival  8564  dffi2  8575  elfiun  8582  tskwe  9066  acndom2  9167  fodomfi2  9173  infpwfien  9175  dfac12lem2  9258  ackbij1lem9  9342  ackbij1lem10  9343  ackbij1lem11  9344  ackbij1lem16  9349  ackbij2lem3  9355  cfss  9379  fin23lem7  9430  fin23lem11  9431  enfin2i  9435  isf32lem8  9474  isf34lem4  9491  isf34lem7  9493  isf34lem6  9494  isfin1-3  9500  fin1a2lem13  9526  ttukeylem6  9628  uzssz  11931  elfzoelz  12701  ackbijnn  14789  incexclem  14797  smuval2  15430  smupvallem  15431  smueqlem  15438  ramub1lem1  15954  ramub1lem2  15955  restid2  16303  mress  16465  mrcuni  16493  mreexexlem4d  16519  mreexexd  16520  mreexdomd  16521  acsfn  16531  isdrs2  17151  ipodrsima  17377  isacs3lem  17378  acsfiindd  17389  lagsubg2  17864  cntzrcl  17968  sylow1lem2  18222  sylow1lem3  18223  sylow1lem4  18224  sylow2alem2  18241  sylow2a  18242  lsmpropd  18298  lssacs  19181  lssacsex  19359  lbsextlem2  19375  lbsextlem3  19376  lbsextlem4  19377  elocv  20230  ppttop  21033  epttop  21035  clsval2  21076  mretopd  21118  neiss2  21127  neiptopnei  21158  ordtbas  21218  subbascn  21280  discmp  21423  uncmp  21428  conncompconn  21457  1stcfb  21470  2ndcdisj  21481  restnlly  21507  nllyrest  21511  nllyidm  21514  cldllycmp  21520  1stckgenlem  21578  dfac14  21643  xkoccn  21644  txnlly  21662  txkgen  21677  xkopt  21680  xkoco2cn  21683  xkoinjcn  21712  tgqtop  21737  nrmhmph  21819  fbelss  21858  fbssfi  21862  infil  21888  alexsubALTlem3  22074  alexsubALTlem4  22075  ustssxp  22229  trust  22254  utopsnneiplem  22272  blssm  22444  blin2  22455  metustss  22577  metustfbas  22583  metust  22584  psmetutop  22593  restmetu  22596  icccmplem2  22847  cncfrss  22915  cncfrss2  22916  bndth  22978  lebnum  22984  ovolicc2  23513  vitalilem5  23603  i1fd  23672  dvbsss  23890  perfdvf  23891  plybss  24174  wilthlem2  25019  f1otrg  25975  uhgrss  26183  upgrss  26207  usgrss  26294  eupth2lems  27421  ubthlem1  28064  elpwdifcl  29693  elpwiuncl  29694  ssnnssfz  29886  indf1ofs  30423  esumval  30443  esumel  30444  gsumesum  30456  esumlub  30457  esumpcvgval  30475  esumcvg  30483  elsigass  30523  ispisys2  30551  sigapildsyslem  30559  sigapildsys  30560  ldgenpisyslem1  30561  ldgenpisys  30564  dynkin  30565  rossspw  30567  srossspw  30574  ddemeas  30634  br2base  30666  sxbrsigalem0  30668  dya2iocucvr  30681  sxbrsigalem2  30683  sxbrsiga  30687  oms0  30694  omssubadd  30697  carsguni  30705  elcarsgss  30706  carsggect  30715  omsmeas  30720  eulerpartlemgvv  30773  coinfliplem  30875  ballotlemfmpn  30891  cvmliftmolem2  31596  cvmlift3lem8  31640  neibastop1  32684  neibastop2lem  32685  neibastop2  32686  filnetlem4  32706  cnambfre  33776  heiborlem3  33929  heiborlem5  33931  heiborlem6  33932  heiborlem10  33936  heibor  33937  mapd1o  37434  elrfi  37764  elrfirn  37765  elrfirn2  37766  ismrcd1  37768  istopclsd  37770  mrefg3  37778  aomclem2  38131  lsmfgcl  38150  lmhmfgima  38160  elmnc  38212  rfovcnvf1od  38803  rfovcnvfvd  38806  fsovrfovd  38808  fsovcnvlem  38812  dssmapnvod  38819  ntrk0kbimka  38842  clsk3nimkb  38843  neik0pk1imk0  38850  ntrclsfveq1  38863  ntrclsfveq2  38864  ntrclsfveq  38865  ntrclsss  38866  ntrclsiso  38870  ntrclsk2  38871  ntrclskb  38872  ntrclsk3  38873  ntrclsk13  38874  ntrclsk4  38875  ntrneifv3  38885  ntrneineine0lem  38886  ntrneineine1lem  38887  ntrneifv4  38888  ntrneiel2  38889  ntrneicls00  38892  ntrneicls11  38893  ntrneiiso  38894  ntrneik2  38895  ntrneikb  38897  ntrneixb  38898  ntrneik3  38899  ntrneix3  38900  ntrneik13  38901  ntrneix13  38902  ntrneik4w  38903  clsneiel2  38912  clsneifv3  38913  clsneifv4  38914  neicvgel2  38923  neicvgfv  38924  gneispb  38934  elpwinss  39714  stoweidlem39  40740  stoweidlem50  40751  sge0resrnlem  41104  sge0iunmptlemre  41116  psmeasurelem  41171  psmeasure  41172  ssnn0ssfz  42700