Theorem elpwid 4569

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-pw 4562

This theorem is used by:  cofon1  8664  cofon2  8665  fopwdom  9087  ssenen  9153  fival  9386  dffi2  9397  elfiun  9404  tskwe  9959  acndom2  10061  fodomfi2  10067  infpwfien  10069  dfac12lem2  10151  ackbij1lem9  10233  ackbij1lem10  10234  ackbij1lem11  10235  ackbij1lem16  10240  ackbij2lem3  10246  cfss  10271  fin23lem7  10322  fin23lem11  10323  enfin2i  10327  isf32lem8  10366  isf34lem4  10383  isf34lem7  10385  isf34lem6  10386  isfin1-3  10392  fin1a2lem13  10418  ttukeylem6  10520  uzssz  12912  elfzoelz  13718  ackbijnn  15921  incexclem  15929  smuval2  16578  smupvallem  16579  smueqlem  16586  ramub1lem1  17124  ramub1lem2  17125  restid2  17521  mress  17683  mrcuni  17715  mreexexlem4d  17741  mreexexd  17742  mreexdomd  17743  isacs2  17747  acsfn  17753  isdrs2  18400  ipodrsima  18635  isacs3lem  18636  acsfiindd  18647  lagsubg2  19328  ghmqusnsg  19415  ghmquskerlem3  19419  ghmqusker  19420  cntzrcl  19460  sylow1lem2  19732  sylow1lem3  19733  sylow1lem4  19734  sylow2alem2  19751  sylow2a  19752  lsmpropd  19810  lssacs  21157  lssacsex  21337  lbsextlem2  21352  lbsextlem3  21353  lbsextlem4  21354  rhmqusnsg  21494  elocv  21887  ppttop  23238  epttop  23240  clsval2  23281  mretopd  23323  neiss2  23332  neiptopnei  23363  ordtbas  23423  subbascn  23485  discmp  23629  uncmp  23634  conncompconn  23663  1stcfb  23676  2ndcdisj  23688  restnlly  23714  nllyrest  23718  nllyidm  23721  cldllycmp  23727  1stckgenlem  23785  dfac14  23850  xkoccn  23851  txnlly  23869  txkgen  23884  xkopt  23887  xkoco2cn  23890  xkoinjcn  23919  tgqtop  23944  nrmhmph  24026  fbelss  24065  fbssfi  24069  infil  24095  alexsubALTlem3  24281  alexsubALTlem4  24282  ustssxp  24437  trust  24461  utopsnneiplem  24479  blssm  24650  blin2  24661  metustss  24783  metust  24790  psmetutop  24799  restmetu  24802  icccmplem2  25056  cncfrss  25125  cncfrss2  25126  bndth  25192  lebnum  25198  ovolicc2  25756  vitalilem5  25846  i1fd  25915  dvbsss  26136  perfdvf  26137  plybss  26426  wilthlem2  27313  oldf  28110  newf  28111  leftf  28128  rightf  28129  elmade  28130  sltsleft  28133  sltsright  28134  cofslts  28191  coinitslts  28192  f1otrg  29335  uhgrss  29529  upgrss  29553  usgrss  29642  eupth2lems  30726  ubthlem1  31359  elpwdifcl  33009  elpwiuncl  33010  ssnnssfz  33266  indf1ofs  33320  pwrssmgc  33448  trsp2cyc  33571  lmhmqusker  33854  rhmquskerlem  33861  esplylem  34084  esplymhp  34086  esplyfv1  34087  esplyfv  34088  esplyfval3  34090  exsslsb  34115  zarcmplem  34399  esumval  34564  esumel  34565  gsumesum  34577  esumlub  34578  esumpcvgval  34596  esumcvg  34604  elsigass  34643  ispisys2  34672  sigapildsyslem  34680  sigapildsys  34681  ldgenpisyslem1  34682  ldgenpisys  34685  dynkin  34686  rossspw  34688  srossspw  34695  ddemeas  34755  br2base  34788  sxbrsigalem0  34790  dya2iocucvr  34803  sxbrsigalem2  34805  sxbrsiga  34809  oms0  34816  omssubadd  34819  carsguni  34827  elcarsgss  34828  carsggect  34837  omsmeas  34842  eulerpartlemgvv  34895  coinfliplem  34998  ballotlemfmpn  35014  cvmliftmolem2  35869  cvmlift3lem8  35913  neibastop1  36986  neibastop2lem  36987  neibastop2  36988  filnetlem4  37008  cnambfre  38425  heiborlem3  38571  heiborlem5  38573  heiborlem6  38574  heiborlem10  38578  heibor  38579  mapd1o  42529  sticksstones3  43022  prjcrv0  43487  elrfi  43547  elrfirn  43548  elrfirn2  43549  ismrcd1  43551  istopclsd  43553  mrefg3  43561  aomclem2  43904  lsmfgcl  43923  lmhmfgima  43933  elmnc  43985  fpwfvss  44260  rfovcnvf1od  44852  rfovcnvfvd  44855  fsovrfovd  44857  fsovcnvlem  44861  dssmapnvod  44868  ntrk0kbimka  44887  clsk3nimkb  44888  neik0pk1imk0  44895  ntrclsfveq1  44908  ntrclsfveq2  44909  ntrclsfveq  44910  ntrclsss  44911  ntrclsiso  44915  ntrclsk2  44916  ntrclskb  44917  ntrclsk3  44918  ntrclsk13  44919  ntrclsk4  44920  ntrneifv3  44930  ntrneineine0lem  44931  ntrneineine1lem  44932  ntrneifv4  44933  ntrneiel2  44934  ntrneicls00  44937  ntrneicls11  44938  ntrneiiso  44939  ntrneik2  44940  ntrneikb  44942  ntrneixb  44943  ntrneik3  44944  ntrneix3  44945  ntrneik13  44946  ntrneix13  44947  ntrneik4w  44948  clsneiel2  44957  clsneifv3  44958  clsneifv4  44959  neicvgel2  44968  neicvgfv  44969  gneispb  44979  elpwinss  45891  stoweidlem39  46875  stoweidlem50  46886  sge0resrnlem  47239  sge0iunmptlemre  47251  psmeasurelem  47306  psmeasure  47307  tmachlem-agreeprod  47773  tmachlem-exagreecover  47782  isubgrvtxuhgr  48788  isuspgrim0  48818  isuspgrimlem  48819  uhgrimisgrgriclem  48854  ssnn0ssfz  49287  iscnrm3rlem3  49876  iscnrm3rlem8  49881  iscnrm3llem1  49883  iscnrm3llem2  49884  iscnrm3l  49885  pgindlem  50649