Theorem elpwid 4631

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  cofon1  8728  cofon2  8729  fopwdom  9146  ssenen  9217  fival  9481  dffi2  9492  elfiun  9499  tskwe  10019  acndom2  10123  fodomfi2  10129  infpwfien  10131  dfac12lem2  10214  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1lem11  10298  ackbij1lem16  10303  ackbij2lem3  10309  cfss  10334  fin23lem7  10385  fin23lem11  10386  enfin2i  10390  isf32lem8  10429  isf34lem4  10446  isf34lem7  10448  isf34lem6  10449  isfin1-3  10455  fin1a2lem13  10481  ttukeylem6  10583  uzssz  12924  elfzoelz  13716  ackbijnn  15876  incexclem  15884  smuval2  16528  smupvallem  16529  smueqlem  16536  ramub1lem1  17073  ramub1lem2  17074  restid2  17490  mress  17651  mrcuni  17679  mreexexlem4d  17705  mreexexd  17706  mreexdomd  17707  isacs2  17711  acsfn  17717  isdrs2  18376  ipodrsima  18611  isacs3lem  18612  acsfiindd  18623  lagsubg2  19234  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  cntzrcl  19367  sylow1lem2  19641  sylow1lem3  19642  sylow1lem4  19643  sylow2alem2  19660  sylow2a  19661  lsmpropd  19719  lssacs  20988  lssacsex  21169  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  rhmqusnsg  21318  elocv  21709  ppttop  23035  epttop  23037  clsval2  23079  mretopd  23121  neiss2  23130  neiptopnei  23161  ordtbas  23221  subbascn  23283  discmp  23427  uncmp  23432  conncompconn  23461  1stcfb  23474  2ndcdisj  23485  restnlly  23511  nllyrest  23515  nllyidm  23518  cldllycmp  23524  1stckgenlem  23582  dfac14  23647  xkoccn  23648  txnlly  23666  txkgen  23681  xkopt  23684  xkoco2cn  23687  xkoinjcn  23716  tgqtop  23741  nrmhmph  23823  fbelss  23862  fbssfi  23866  infil  23892  alexsubALTlem3  24078  alexsubALTlem4  24079  ustssxp  24234  trust  24259  utopsnneiplem  24277  blssm  24449  blin2  24460  metustss  24585  metust  24592  psmetutop  24601  restmetu  24604  icccmplem2  24864  cncfrss  24936  cncfrss2  24937  bndth  25009  lebnum  25015  ovolicc2  25576  vitalilem5  25666  i1fd  25735  dvbsss  25957  perfdvf  25958  plybss  26253  wilthlem2  27130  oldf  27914  newf  27915  leftf  27922  rightf  27923  elmade  27924  ssltleft  27927  ssltright  27928  cofsslt  27970  coinitsslt  27971  f1otrg  28897  uhgrss  29099  upgrss  29123  usgrss  29209  eupth2lems  30270  ubthlem1  30902  elpwdifcl  32556  elpwiuncl  32557  ssnnssfz  32792  pwrssmgc  32973  trsp2cyc  33116  lmhmqusker  33410  rhmquskerlem  33418  zarcmplem  33827  indf1ofs  33990  esumval  34010  esumel  34011  gsumesum  34023  esumlub  34024  esumpcvgval  34042  esumcvg  34050  elsigass  34089  ispisys2  34117  sigapildsyslem  34125  sigapildsys  34126  ldgenpisyslem1  34127  ldgenpisys  34130  dynkin  34131  rossspw  34133  srossspw  34140  ddemeas  34200  br2base  34234  sxbrsigalem0  34236  dya2iocucvr  34249  sxbrsigalem2  34251  sxbrsiga  34255  oms0  34262  omssubadd  34265  carsguni  34273  elcarsgss  34274  carsggect  34283  omsmeas  34288  eulerpartlemgvv  34341  coinfliplem  34443  ballotlemfmpn  34459  cvmliftmolem2  35250  cvmlift3lem8  35294  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  filnetlem4  36347  cnambfre  37628  heiborlem3  37773  heiborlem5  37775  heiborlem6  37776  heiborlem10  37780  heibor  37781  mapd1o  41605  sticksstones3  42105  prjcrv0  42588  elrfi  42650  elrfirn  42651  elrfirn2  42652  ismrcd1  42654  istopclsd  42656  mrefg3  42664  aomclem2  43012  lsmfgcl  43031  lmhmfgima  43041  elmnc  43093  fpwfvss  43374  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  fsovcnvlem  43975  dssmapnvod  43982  ntrk0kbimka  44001  clsk3nimkb  44002  neik0pk1imk0  44009  ntrclsfveq1  44022  ntrclsfveq2  44023  ntrclsfveq  44024  ntrclsss  44025  ntrclsiso  44029  ntrclsk2  44030  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrclsk4  44034  ntrneifv3  44044  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneifv4  44047  ntrneiel2  44048  ntrneicls00  44051  ntrneicls11  44052  ntrneiiso  44053  ntrneik2  44054  ntrneikb  44056  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  ntrneik4w  44062  clsneiel2  44071  clsneifv3  44072  clsneifv4  44073  neicvgel2  44082  neicvgfv  44083  gneispb  44093  elpwinss  44951  stoweidlem39  45960  stoweidlem50  45971  sge0resrnlem  46324  sge0iunmptlemre  46336  psmeasurelem  46391  psmeasure  46392  isubgrvtxuhgr  47736  isuspgrim0  47756  isuspgrimlem  47758  uhgrimisgrgriclem  47782  ssnn0ssfz  48074  iscnrm3rlem3  48622  iscnrm3rlem8  48627  iscnrm3llem1  48629  iscnrm3llem2  48630  iscnrm3l  48631  pgindlem  48807