Theorem elpwid 4562

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  cofon1  8597  cofon2  8598  fopwdom  9009  ssenen  9075  fival  9321  dffi2  9332  elfiun  9339  tskwe  9865  acndom2  9967  fodomfi2  9973  infpwfien  9975  dfac12lem2  10058  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem11  10142  ackbij1lem16  10147  ackbij2lem3  10153  cfss  10178  fin23lem7  10229  fin23lem11  10230  enfin2i  10234  isf32lem8  10273  isf34lem4  10290  isf34lem7  10292  isf34lem6  10293  isfin1-3  10299  fin1a2lem13  10325  ttukeylem6  10427  uzssz  12774  elfzoelz  13580  ackbijnn  15753  incexclem  15761  smuval2  16411  smupvallem  16412  smueqlem  16419  ramub1lem1  16956  ramub1lem2  16957  restid2  17352  mress  17513  mrcuni  17545  mreexexlem4d  17571  mreexexd  17572  mreexdomd  17573  isacs2  17577  acsfn  17583  isdrs2  18230  ipodrsima  18465  isacs3lem  18466  acsfiindd  18477  lagsubg2  19091  ghmqusnsg  19179  ghmquskerlem3  19183  ghmqusker  19184  cntzrcl  19224  sylow1lem2  19496  sylow1lem3  19497  sylow1lem4  19498  sylow2alem2  19515  sylow2a  19516  lsmpropd  19574  lssacs  20888  lssacsex  21069  lbsextlem2  21084  lbsextlem3  21085  lbsextlem4  21086  rhmqusnsg  21210  elocv  21593  ppttop  22910  epttop  22912  clsval2  22953  mretopd  22995  neiss2  23004  neiptopnei  23035  ordtbas  23095  subbascn  23157  discmp  23301  uncmp  23306  conncompconn  23335  1stcfb  23348  2ndcdisj  23359  restnlly  23385  nllyrest  23389  nllyidm  23392  cldllycmp  23398  1stckgenlem  23456  dfac14  23521  xkoccn  23522  txnlly  23540  txkgen  23555  xkopt  23558  xkoco2cn  23561  xkoinjcn  23590  tgqtop  23615  nrmhmph  23697  fbelss  23736  fbssfi  23740  infil  23766  alexsubALTlem3  23952  alexsubALTlem4  23953  ustssxp  24108  trust  24133  utopsnneiplem  24151  blssm  24322  blin2  24333  metustss  24455  metust  24462  psmetutop  24471  restmetu  24474  icccmplem2  24728  cncfrss  24800  cncfrss2  24801  bndth  24873  lebnum  24879  ovolicc2  25439  vitalilem5  25529  i1fd  25598  dvbsss  25819  perfdvf  25820  plybss  26115  wilthlem2  26995  oldf  27785  newf  27786  leftf  27797  rightf  27798  elmade  27799  ssltleft  27802  ssltright  27803  cofsslt  27849  coinitsslt  27850  f1otrg  28834  uhgrss  29027  upgrss  29051  usgrss  29137  eupth2lems  30200  ubthlem1  30832  elpwdifcl  32488  elpwiuncl  32489  ssnnssfz  32743  indf1ofs  32822  pwrssmgc  32955  trsp2cyc  33078  lmhmqusker  33364  rhmquskerlem  33372  exsslsb  33568  zarcmplem  33847  esumval  34012  esumel  34013  gsumesum  34025  esumlub  34026  esumpcvgval  34044  esumcvg  34052  elsigass  34091  ispisys2  34119  sigapildsyslem  34127  sigapildsys  34128  ldgenpisyslem1  34129  ldgenpisys  34132  dynkin  34133  rossspw  34135  srossspw  34142  ddemeas  34202  br2base  34236  sxbrsigalem0  34238  dya2iocucvr  34251  sxbrsigalem2  34253  sxbrsiga  34257  oms0  34264  omssubadd  34267  carsguni  34275  elcarsgss  34276  carsggect  34285  omsmeas  34290  eulerpartlemgvv  34343  coinfliplem  34446  ballotlemfmpn  34462  cvmliftmolem2  35254  cvmlift3lem8  35298  neibastop1  36332  neibastop2lem  36333  neibastop2  36334  filnetlem4  36354  cnambfre  37647  heiborlem3  37792  heiborlem5  37794  heiborlem6  37795  heiborlem10  37799  heibor  37800  mapd1o  41627  sticksstones3  42121  prjcrv0  42606  elrfi  42667  elrfirn  42668  elrfirn2  42669  ismrcd1  42671  istopclsd  42673  mrefg3  42681  aomclem2  43028  lsmfgcl  43047  lmhmfgima  43057  elmnc  43109  fpwfvss  43385  rfovcnvf1od  43977  rfovcnvfvd  43980  fsovrfovd  43982  fsovcnvlem  43986  dssmapnvod  43993  ntrk0kbimka  44012  clsk3nimkb  44013  neik0pk1imk0  44020  ntrclsfveq1  44033  ntrclsfveq2  44034  ntrclsfveq  44035  ntrclsss  44036  ntrclsiso  44040  ntrclsk2  44041  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrclsk4  44045  ntrneifv3  44055  ntrneineine0lem  44056  ntrneineine1lem  44057  ntrneifv4  44058  ntrneiel2  44059  ntrneicls00  44062  ntrneicls11  44063  ntrneiiso  44064  ntrneik2  44065  ntrneikb  44067  ntrneixb  44068  ntrneik3  44069  ntrneix3  44070  ntrneik13  44071  ntrneix13  44072  ntrneik4w  44073  clsneiel2  44082  clsneifv3  44083  clsneifv4  44084  neicvgel2  44093  neicvgfv  44094  gneispb  44104  elpwinss  45027  stoweidlem39  46021  stoweidlem50  46032  sge0resrnlem  46385  sge0iunmptlemre  46397  psmeasurelem  46452  psmeasure  46453  isubgrvtxuhgr  47848  isuspgrim0  47878  isuspgrimlem  47879  uhgrimisgrgriclem  47914  ssnn0ssfz  48321  iscnrm3rlem3  48914  iscnrm3rlem8  48919  iscnrm3llem1  48921  iscnrm3llem2  48922  iscnrm3l  48923  pgindlem  49688