Theorem elpwid 4613

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-pw 4606

This theorem is referenced by:  cofon1  8708  cofon2  8709  fopwdom  9118  ssenen  9189  fival  9449  dffi2  9460  elfiun  9467  tskwe  9987  acndom2  10091  fodomfi2  10097  infpwfien  10099  dfac12lem2  10182  ackbij1lem9  10264  ackbij1lem10  10265  ackbij1lem11  10266  ackbij1lem16  10271  ackbij2lem3  10277  cfss  10302  fin23lem7  10353  fin23lem11  10354  enfin2i  10358  isf32lem8  10397  isf34lem4  10414  isf34lem7  10416  isf34lem6  10417  isfin1-3  10423  fin1a2lem13  10449  ttukeylem6  10551  uzssz  12896  elfzoelz  13695  ackbijnn  15860  incexclem  15868  smuval2  16515  smupvallem  16516  smueqlem  16523  ramub1lem1  17059  ramub1lem2  17060  restid2  17476  mress  17637  mrcuni  17665  mreexexlem4d  17691  mreexexd  17692  mreexdomd  17693  isacs2  17697  acsfn  17703  isdrs2  18363  ipodrsima  18598  isacs3lem  18599  acsfiindd  18610  lagsubg2  19224  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  cntzrcl  19357  sylow1lem2  19631  sylow1lem3  19632  sylow1lem4  19633  sylow2alem2  19650  sylow2a  19651  lsmpropd  19709  lssacs  20982  lssacsex  21163  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  rhmqusnsg  21312  elocv  21703  ppttop  23029  epttop  23031  clsval2  23073  mretopd  23115  neiss2  23124  neiptopnei  23155  ordtbas  23215  subbascn  23277  discmp  23421  uncmp  23426  conncompconn  23455  1stcfb  23468  2ndcdisj  23479  restnlly  23505  nllyrest  23509  nllyidm  23512  cldllycmp  23518  1stckgenlem  23576  dfac14  23641  xkoccn  23642  txnlly  23660  txkgen  23675  xkopt  23678  xkoco2cn  23681  xkoinjcn  23710  tgqtop  23735  nrmhmph  23817  fbelss  23856  fbssfi  23860  infil  23886  alexsubALTlem3  24072  alexsubALTlem4  24073  ustssxp  24228  trust  24253  utopsnneiplem  24271  blssm  24443  blin2  24454  metustss  24579  metust  24586  psmetutop  24595  restmetu  24598  icccmplem2  24858  cncfrss  24930  cncfrss2  24931  bndth  25003  lebnum  25009  ovolicc2  25570  vitalilem5  25660  i1fd  25729  dvbsss  25951  perfdvf  25952  plybss  26247  wilthlem2  27126  oldf  27910  newf  27911  leftf  27918  rightf  27919  elmade  27920  ssltleft  27923  ssltright  27924  cofsslt  27966  coinitsslt  27967  f1otrg  28893  uhgrss  29095  upgrss  29119  usgrss  29205  eupth2lems  30266  ubthlem1  30898  elpwdifcl  32553  elpwiuncl  32554  ssnnssfz  32795  pwrssmgc  32974  trsp2cyc  33125  lmhmqusker  33424  rhmquskerlem  33432  zarcmplem  33841  indf1ofs  34006  esumval  34026  esumel  34027  gsumesum  34039  esumlub  34040  esumpcvgval  34058  esumcvg  34066  elsigass  34105  ispisys2  34133  sigapildsyslem  34141  sigapildsys  34142  ldgenpisyslem1  34143  ldgenpisys  34146  dynkin  34147  rossspw  34149  srossspw  34156  ddemeas  34216  br2base  34250  sxbrsigalem0  34252  dya2iocucvr  34265  sxbrsigalem2  34267  sxbrsiga  34271  oms0  34278  omssubadd  34281  carsguni  34289  elcarsgss  34290  carsggect  34299  omsmeas  34304  eulerpartlemgvv  34357  coinfliplem  34459  ballotlemfmpn  34475  cvmliftmolem2  35266  cvmlift3lem8  35310  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  filnetlem4  36363  cnambfre  37654  heiborlem3  37799  heiborlem5  37801  heiborlem6  37802  heiborlem10  37806  heibor  37807  mapd1o  41630  sticksstones3  42129  prjcrv0  42619  elrfi  42681  elrfirn  42682  elrfirn2  42683  ismrcd1  42685  istopclsd  42687  mrefg3  42695  aomclem2  43043  lsmfgcl  43062  lmhmfgima  43072  elmnc  43124  fpwfvss  43401  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  ntrk0kbimka  44028  clsk3nimkb  44029  neik0pk1imk0  44036  ntrclsfveq1  44049  ntrclsfveq2  44050  ntrclsfveq  44051  ntrclsss  44052  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneifv3  44071  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneifv4  44074  ntrneiel2  44075  ntrneicls00  44078  ntrneicls11  44079  ntrneiiso  44080  ntrneik2  44081  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  clsneiel2  44098  clsneifv3  44099  clsneifv4  44100  neicvgel2  44109  neicvgfv  44110  gneispb  44120  elpwinss  44988  stoweidlem39  45994  stoweidlem50  46005  sge0resrnlem  46358  sge0iunmptlemre  46370  psmeasurelem  46425  psmeasure  46426  isubgrvtxuhgr  47787  isuspgrim0  47809  isuspgrimlem  47811  uhgrimisgrgriclem  47835  ssnn0ssfz  48193  iscnrm3rlem3  48738  iscnrm3rlem8  48743  iscnrm3llem1  48745  iscnrm3llem2  48746  iscnrm3l  48747  pgindlem  48945