Theorem elpwid 4609

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  𝒫 cpw 4600

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602

This theorem is referenced by:  cofon1  8710  cofon2  8711  fopwdom  9120  ssenen  9191  fival  9452  dffi2  9463  elfiun  9470  tskwe  9990  acndom2  10094  fodomfi2  10100  infpwfien  10102  dfac12lem2  10185  ackbij1lem9  10267  ackbij1lem10  10268  ackbij1lem11  10269  ackbij1lem16  10274  ackbij2lem3  10280  cfss  10305  fin23lem7  10356  fin23lem11  10357  enfin2i  10361  isf32lem8  10400  isf34lem4  10417  isf34lem7  10419  isf34lem6  10420  isfin1-3  10426  fin1a2lem13  10452  ttukeylem6  10554  uzssz  12899  elfzoelz  13699  ackbijnn  15864  incexclem  15872  smuval2  16519  smupvallem  16520  smueqlem  16527  ramub1lem1  17064  ramub1lem2  17065  restid2  17475  mress  17636  mrcuni  17664  mreexexlem4d  17690  mreexexd  17691  mreexdomd  17692  isacs2  17696  acsfn  17702  isdrs2  18352  ipodrsima  18586  isacs3lem  18587  acsfiindd  18598  lagsubg2  19212  ghmqusnsg  19300  ghmquskerlem3  19304  ghmqusker  19305  cntzrcl  19345  sylow1lem2  19617  sylow1lem3  19618  sylow1lem4  19619  sylow2alem2  19636  sylow2a  19637  lsmpropd  19695  lssacs  20965  lssacsex  21146  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  rhmqusnsg  21295  elocv  21686  ppttop  23014  epttop  23016  clsval2  23058  mretopd  23100  neiss2  23109  neiptopnei  23140  ordtbas  23200  subbascn  23262  discmp  23406  uncmp  23411  conncompconn  23440  1stcfb  23453  2ndcdisj  23464  restnlly  23490  nllyrest  23494  nllyidm  23497  cldllycmp  23503  1stckgenlem  23561  dfac14  23626  xkoccn  23627  txnlly  23645  txkgen  23660  xkopt  23663  xkoco2cn  23666  xkoinjcn  23695  tgqtop  23720  nrmhmph  23802  fbelss  23841  fbssfi  23845  infil  23871  alexsubALTlem3  24057  alexsubALTlem4  24058  ustssxp  24213  trust  24238  utopsnneiplem  24256  blssm  24428  blin2  24439  metustss  24564  metust  24571  psmetutop  24580  restmetu  24583  icccmplem2  24845  cncfrss  24917  cncfrss2  24918  bndth  24990  lebnum  24996  ovolicc2  25557  vitalilem5  25647  i1fd  25716  dvbsss  25937  perfdvf  25938  plybss  26233  wilthlem2  27112  oldf  27896  newf  27897  leftf  27904  rightf  27905  elmade  27906  ssltleft  27909  ssltright  27910  cofsslt  27952  coinitsslt  27953  f1otrg  28879  uhgrss  29081  upgrss  29105  usgrss  29191  eupth2lems  30257  ubthlem1  30889  elpwdifcl  32545  elpwiuncl  32546  ssnnssfz  32789  indf1ofs  32851  pwrssmgc  32990  trsp2cyc  33143  lmhmqusker  33445  rhmquskerlem  33453  exsslsb  33647  zarcmplem  33880  esumval  34047  esumel  34048  gsumesum  34060  esumlub  34061  esumpcvgval  34079  esumcvg  34087  elsigass  34126  ispisys2  34154  sigapildsyslem  34162  sigapildsys  34163  ldgenpisyslem1  34164  ldgenpisys  34167  dynkin  34168  rossspw  34170  srossspw  34177  ddemeas  34237  br2base  34271  sxbrsigalem0  34273  dya2iocucvr  34286  sxbrsigalem2  34288  sxbrsiga  34292  oms0  34299  omssubadd  34302  carsguni  34310  elcarsgss  34311  carsggect  34320  omsmeas  34325  eulerpartlemgvv  34378  coinfliplem  34481  ballotlemfmpn  34497  cvmliftmolem2  35287  cvmlift3lem8  35331  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  filnetlem4  36382  cnambfre  37675  heiborlem3  37820  heiborlem5  37822  heiborlem6  37823  heiborlem10  37827  heibor  37828  mapd1o  41650  sticksstones3  42149  prjcrv0  42643  elrfi  42705  elrfirn  42706  elrfirn2  42707  ismrcd1  42709  istopclsd  42711  mrefg3  42719  aomclem2  43067  lsmfgcl  43086  lmhmfgima  43096  elmnc  43148  fpwfvss  43425  rfovcnvf1od  44017  rfovcnvfvd  44020  fsovrfovd  44022  fsovcnvlem  44026  dssmapnvod  44033  ntrk0kbimka  44052  clsk3nimkb  44053  neik0pk1imk0  44060  ntrclsfveq1  44073  ntrclsfveq2  44074  ntrclsfveq  44075  ntrclsss  44076  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrclsk4  44085  ntrneifv3  44095  ntrneineine0lem  44096  ntrneineine1lem  44097  ntrneifv4  44098  ntrneiel2  44099  ntrneicls00  44102  ntrneicls11  44103  ntrneiiso  44104  ntrneik2  44105  ntrneikb  44107  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  ntrneik4w  44113  clsneiel2  44122  clsneifv3  44123  clsneifv4  44124  neicvgel2  44133  neicvgfv  44134  gneispb  44144  elpwinss  45054  stoweidlem39  46054  stoweidlem50  46065  sge0resrnlem  46418  sge0iunmptlemre  46430  psmeasurelem  46485  psmeasure  46486  isubgrvtxuhgr  47850  isuspgrim0  47872  isuspgrimlem  47874  uhgrimisgrgriclem  47898  ssnn0ssfz  48265  iscnrm3rlem3  48839  iscnrm3rlem8  48844  iscnrm3llem1  48846  iscnrm3llem2  48847  iscnrm3l  48848  pgindlem  49234