Theorem elpwid 4564

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3902  𝒫 cpw 4555

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3919  df-pw 4557

This theorem is referenced by:  cofon1  8602  cofon2  8603  fopwdom  9017  ssenen  9083  fival  9319  dffi2  9330  elfiun  9337  tskwe  9866  acndom2  9968  fodomfi2  9974  infpwfien  9976  dfac12lem2  10059  ackbij1lem9  10141  ackbij1lem10  10142  ackbij1lem11  10143  ackbij1lem16  10148  ackbij2lem3  10154  cfss  10179  fin23lem7  10230  fin23lem11  10231  enfin2i  10235  isf32lem8  10274  isf34lem4  10291  isf34lem7  10293  isf34lem6  10294  isfin1-3  10300  fin1a2lem13  10326  ttukeylem6  10428  uzssz  12776  elfzoelz  13579  ackbijnn  15755  incexclem  15763  smuval2  16413  smupvallem  16414  smueqlem  16421  ramub1lem1  16958  ramub1lem2  16959  restid2  17354  mress  17516  mrcuni  17548  mreexexlem4d  17574  mreexexd  17575  mreexdomd  17576  isacs2  17580  acsfn  17586  isdrs2  18233  ipodrsima  18468  isacs3lem  18469  acsfiindd  18480  lagsubg2  19127  ghmqusnsg  19215  ghmquskerlem3  19219  ghmqusker  19220  cntzrcl  19260  sylow1lem2  19532  sylow1lem3  19533  sylow1lem4  19534  sylow2alem2  19551  sylow2a  19552  lsmpropd  19610  lssacs  20922  lssacsex  21103  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  rhmqusnsg  21244  elocv  21627  ppttop  22955  epttop  22957  clsval2  22998  mretopd  23040  neiss2  23049  neiptopnei  23080  ordtbas  23140  subbascn  23202  discmp  23346  uncmp  23351  conncompconn  23380  1stcfb  23393  2ndcdisj  23404  restnlly  23430  nllyrest  23434  nllyidm  23437  cldllycmp  23443  1stckgenlem  23501  dfac14  23566  xkoccn  23567  txnlly  23585  txkgen  23600  xkopt  23603  xkoco2cn  23606  xkoinjcn  23635  tgqtop  23660  nrmhmph  23742  fbelss  23781  fbssfi  23785  infil  23811  alexsubALTlem3  23997  alexsubALTlem4  23998  ustssxp  24153  trust  24177  utopsnneiplem  24195  blssm  24366  blin2  24377  metustss  24499  metust  24506  psmetutop  24515  restmetu  24518  icccmplem2  24772  cncfrss  24844  cncfrss2  24845  bndth  24917  lebnum  24923  ovolicc2  25483  vitalilem5  25573  i1fd  25642  dvbsss  25863  perfdvf  25864  plybss  26159  wilthlem2  27039  oldf  27835  newf  27836  leftf  27847  rightf  27848  elmade  27849  ssltleft  27852  ssltright  27853  cofsslt  27900  coinitsslt  27901  f1otrg  28926  uhgrss  29120  upgrss  29144  usgrss  29230  eupth2lems  30296  ubthlem1  30928  elpwdifcl  32583  elpwiuncl  32584  ssnnssfz  32848  indf1ofs  32929  pwrssmgc  33063  trsp2cyc  33186  lmhmqusker  33479  rhmquskerlem  33487  esplylem  33705  esplymhp  33707  esplyfv1  33708  esplyfv  33709  esplyfval3  33711  exsslsb  33734  zarcmplem  34019  esumval  34184  esumel  34185  gsumesum  34197  esumlub  34198  esumpcvgval  34216  esumcvg  34224  elsigass  34263  ispisys2  34291  sigapildsyslem  34299  sigapildsys  34300  ldgenpisyslem1  34301  ldgenpisys  34304  dynkin  34305  rossspw  34307  srossspw  34314  ddemeas  34374  br2base  34407  sxbrsigalem0  34409  dya2iocucvr  34422  sxbrsigalem2  34424  sxbrsiga  34428  oms0  34435  omssubadd  34438  carsguni  34446  elcarsgss  34447  carsggect  34456  omsmeas  34461  eulerpartlemgvv  34514  coinfliplem  34617  ballotlemfmpn  34633  cvmliftmolem2  35457  cvmlift3lem8  35501  neibastop1  36534  neibastop2lem  36535  neibastop2  36536  filnetlem4  36556  cnambfre  37840  heiborlem3  37985  heiborlem5  37987  heiborlem6  37988  heiborlem10  37992  heibor  37993  mapd1o  41945  sticksstones3  42439  prjcrv0  42912  elrfi  42972  elrfirn  42973  elrfirn2  42974  ismrcd1  42976  istopclsd  42978  mrefg3  42986  aomclem2  43333  lsmfgcl  43352  lmhmfgima  43362  elmnc  43414  fpwfvss  43689  rfovcnvf1od  44281  rfovcnvfvd  44284  fsovrfovd  44286  fsovcnvlem  44290  dssmapnvod  44297  ntrk0kbimka  44316  clsk3nimkb  44317  neik0pk1imk0  44324  ntrclsfveq1  44337  ntrclsfveq2  44338  ntrclsfveq  44339  ntrclsss  44340  ntrclsiso  44344  ntrclsk2  44345  ntrclskb  44346  ntrclsk3  44347  ntrclsk13  44348  ntrclsk4  44349  ntrneifv3  44359  ntrneineine0lem  44360  ntrneineine1lem  44361  ntrneifv4  44362  ntrneiel2  44363  ntrneicls00  44366  ntrneicls11  44367  ntrneiiso  44368  ntrneik2  44369  ntrneikb  44371  ntrneixb  44372  ntrneik3  44373  ntrneix3  44374  ntrneik13  44375  ntrneix13  44376  ntrneik4w  44377  clsneiel2  44386  clsneifv3  44387  clsneifv4  44388  neicvgel2  44397  neicvgfv  44398  gneispb  44408  elpwinss  45330  stoweidlem39  46319  stoweidlem50  46330  sge0resrnlem  46683  sge0iunmptlemre  46695  psmeasurelem  46750  psmeasure  46751  isubgrvtxuhgr  48146  isuspgrim0  48176  isuspgrimlem  48177  uhgrimisgrgriclem  48212  ssnn0ssfz  48631  iscnrm3rlem3  49223  iscnrm3rlem8  49228  iscnrm3llem1  49230  iscnrm3llem2  49231  iscnrm3l  49232  pgindlem  49996