Theorem elpwid 4545

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  fopwdom  8876  ssenen  8947  fival  9180  dffi2  9191  elfiun  9198  tskwe  9717  acndom2  9819  fodomfi2  9825  infpwfien  9827  dfac12lem2  9909  ackbij1lem9  9993  ackbij1lem10  9994  ackbij1lem11  9995  ackbij1lem16  10000  ackbij2lem3  10006  cfss  10030  fin23lem7  10081  fin23lem11  10082  enfin2i  10086  isf32lem8  10125  isf34lem4  10142  isf34lem7  10144  isf34lem6  10145  isfin1-3  10151  fin1a2lem13  10177  ttukeylem6  10279  uzssz  12612  elfzoelz  13396  ackbijnn  15549  incexclem  15557  smuval2  16198  smupvallem  16199  smueqlem  16206  ramub1lem1  16736  ramub1lem2  16737  restid2  17150  mress  17311  mrcuni  17339  mreexexlem4d  17365  mreexexd  17366  mreexdomd  17367  isacs2  17371  acsfn  17377  isdrs2  18033  ipodrsima  18268  isacs3lem  18269  acsfiindd  18280  lagsubg2  18826  cntzrcl  18942  sylow1lem2  19213  sylow1lem3  19214  sylow1lem4  19215  sylow2alem2  19232  sylow2a  19233  lsmpropd  19292  lssacs  20238  lssacsex  20415  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  elocv  20882  ppttop  22166  epttop  22168  clsval2  22210  mretopd  22252  neiss2  22261  neiptopnei  22292  ordtbas  22352  subbascn  22414  discmp  22558  uncmp  22563  conncompconn  22592  1stcfb  22605  2ndcdisj  22616  restnlly  22642  nllyrest  22646  nllyidm  22649  cldllycmp  22655  1stckgenlem  22713  dfac14  22778  xkoccn  22779  txnlly  22797  txkgen  22812  xkopt  22815  xkoco2cn  22818  xkoinjcn  22847  tgqtop  22872  nrmhmph  22954  fbelss  22993  fbssfi  22997  infil  23023  alexsubALTlem3  23209  alexsubALTlem4  23210  ustssxp  23365  trust  23390  utopsnneiplem  23408  blssm  23580  blin2  23591  metustss  23716  metust  23723  psmetutop  23732  restmetu  23735  icccmplem2  23995  cncfrss  24063  cncfrss2  24064  bndth  24130  lebnum  24136  ovolicc2  24695  vitalilem5  24785  i1fd  24854  dvbsss  25075  perfdvf  25076  plybss  25364  wilthlem2  26227  f1otrg  27241  uhgrss  27443  upgrss  27467  usgrss  27553  eupth2lems  28611  ubthlem1  29241  elpwdifcl  30884  elpwiuncl  30885  ssnnssfz  31117  pwrssmgc  31287  trsp2cyc  31399  zarcmplem  31840  indf1ofs  32003  esumval  32023  esumel  32024  gsumesum  32036  esumlub  32037  esumpcvgval  32055  esumcvg  32063  elsigass  32102  ispisys2  32130  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  ldgenpisys  32143  dynkin  32144  rossspw  32146  srossspw  32153  ddemeas  32213  br2base  32245  sxbrsigalem0  32247  dya2iocucvr  32260  sxbrsigalem2  32262  sxbrsiga  32266  oms0  32273  omssubadd  32276  carsguni  32284  elcarsgss  32285  carsggect  32294  omsmeas  32299  eulerpartlemgvv  32352  coinfliplem  32454  ballotlemfmpn  32470  cvmliftmolem2  33253  cvmlift3lem8  33297  oldf  34050  newf  34051  leftf  34058  rightf  34059  elmade  34060  ssltleft  34063  ssltright  34064  cofsslt  34097  coinitsslt  34098  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  filnetlem4  34579  cnambfre  35834  heiborlem3  35980  heiborlem5  35982  heiborlem6  35983  heiborlem10  35987  heibor  35988  mapd1o  39669  sticksstones3  40111  elrfi  40523  elrfirn  40524  elrfirn2  40525  ismrcd1  40527  istopclsd  40529  mrefg3  40537  aomclem2  40887  lsmfgcl  40906  lmhmfgima  40916  elmnc  40968  rfovcnvf1od  41619  rfovcnvfvd  41622  fsovrfovd  41624  fsovcnvlem  41628  dssmapnvod  41635  ntrk0kbimka  41656  clsk3nimkb  41657  neik0pk1imk0  41664  ntrclsfveq1  41677  ntrclsfveq2  41678  ntrclsfveq  41679  ntrclsss  41680  ntrclsiso  41684  ntrclsk2  41685  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrclsk4  41689  ntrneifv3  41699  ntrneineine0lem  41700  ntrneineine1lem  41701  ntrneifv4  41702  ntrneiel2  41703  ntrneicls00  41706  ntrneicls11  41707  ntrneiiso  41708  ntrneik2  41709  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4w  41717  clsneiel2  41726  clsneifv3  41727  clsneifv4  41728  neicvgel2  41737  neicvgfv  41738  gneispb  41748  elpwinss  42604  stoweidlem39  43587  stoweidlem50  43598  sge0resrnlem  43948  sge0iunmptlemre  43960  psmeasurelem  44015  psmeasure  44016  ssnn0ssfz  45696  iscnrm3rlem3  46247  iscnrm3rlem8  46252  iscnrm3llem1  46254  iscnrm3llem2  46255  iscnrm3l  46256