Theorem elpwid 4615

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3946  𝒫 cpw 4606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3963  df-pw 4608

This theorem is referenced by:  cofon1  8701  cofon2  8702  fopwdom  9117  ssenen  9188  fival  9451  dffi2  9462  elfiun  9469  tskwe  9989  acndom2  10093  fodomfi2  10099  infpwfien  10101  dfac12lem2  10183  ackbij1lem9  10267  ackbij1lem10  10268  ackbij1lem11  10269  ackbij1lem16  10274  ackbij2lem3  10280  cfss  10304  fin23lem7  10355  fin23lem11  10356  enfin2i  10360  isf32lem8  10399  isf34lem4  10416  isf34lem7  10418  isf34lem6  10419  isfin1-3  10425  fin1a2lem13  10451  ttukeylem6  10553  uzssz  12890  elfzoelz  13681  ackbijnn  15827  incexclem  15835  smuval2  16477  smupvallem  16478  smueqlem  16485  ramub1lem1  17023  ramub1lem2  17024  restid2  17440  mress  17601  mrcuni  17629  mreexexlem4d  17655  mreexexd  17656  mreexdomd  17657  isacs2  17661  acsfn  17667  isdrs2  18326  ipodrsima  18561  isacs3lem  18562  acsfiindd  18573  lagsubg2  19183  ghmqusnsg  19271  ghmquskerlem3  19275  ghmqusker  19276  cntzrcl  19316  sylow1lem2  19592  sylow1lem3  19593  sylow1lem4  19594  sylow2alem2  19611  sylow2a  19612  lsmpropd  19670  lssacs  20891  lssacsex  21072  lbsextlem2  21087  lbsextlem3  21088  lbsextlem4  21089  rhmqusnsg  21221  elocv  21656  ppttop  22993  epttop  22995  clsval2  23037  mretopd  23079  neiss2  23088  neiptopnei  23119  ordtbas  23179  subbascn  23241  discmp  23385  uncmp  23390  conncompconn  23419  1stcfb  23432  2ndcdisj  23443  restnlly  23469  nllyrest  23473  nllyidm  23476  cldllycmp  23482  1stckgenlem  23540  dfac14  23605  xkoccn  23606  txnlly  23624  txkgen  23639  xkopt  23642  xkoco2cn  23645  xkoinjcn  23674  tgqtop  23699  nrmhmph  23781  fbelss  23820  fbssfi  23824  infil  23850  alexsubALTlem3  24036  alexsubALTlem4  24037  ustssxp  24192  trust  24217  utopsnneiplem  24235  blssm  24407  blin2  24418  metustss  24543  metust  24550  psmetutop  24559  restmetu  24562  icccmplem2  24822  cncfrss  24894  cncfrss2  24895  bndth  24967  lebnum  24973  ovolicc2  25534  vitalilem5  25624  i1fd  25693  dvbsss  25914  perfdvf  25915  plybss  26213  wilthlem2  27089  oldf  27873  newf  27874  leftf  27881  rightf  27882  elmade  27883  ssltleft  27886  ssltright  27887  cofsslt  27927  coinitsslt  27928  f1otrg  28790  uhgrss  28992  upgrss  29016  usgrss  29102  eupth2lems  30163  ubthlem1  30795  elpwdifcl  32444  elpwiuncl  32445  ssnnssfz  32678  pwrssmgc  32858  trsp2cyc  32978  lmhmqusker  33269  rhmquskerlem  33277  zarcmplem  33652  indf1ofs  33815  esumval  33835  esumel  33836  gsumesum  33848  esumlub  33849  esumpcvgval  33867  esumcvg  33875  elsigass  33914  ispisys2  33942  sigapildsyslem  33950  sigapildsys  33951  ldgenpisyslem1  33952  ldgenpisys  33955  dynkin  33956  rossspw  33958  srossspw  33965  ddemeas  34025  br2base  34059  sxbrsigalem0  34061  dya2iocucvr  34074  sxbrsigalem2  34076  sxbrsiga  34080  oms0  34087  omssubadd  34090  carsguni  34098  elcarsgss  34099  carsggect  34108  omsmeas  34113  eulerpartlemgvv  34166  coinfliplem  34268  ballotlemfmpn  34284  cvmliftmolem2  35062  cvmlift3lem8  35106  neibastop1  36019  neibastop2lem  36020  neibastop2  36021  filnetlem4  36041  cnambfre  37317  heiborlem3  37462  heiborlem5  37464  heiborlem6  37465  heiborlem10  37469  heibor  37470  mapd1o  41295  sticksstones3  41794  prjcrv0  42224  elrfi  42288  elrfirn  42289  elrfirn2  42290  ismrcd1  42292  istopclsd  42294  mrefg3  42302  aomclem2  42653  lsmfgcl  42672  lmhmfgima  42682  elmnc  42734  fpwfvss  43016  rfovcnvf1od  43608  rfovcnvfvd  43611  fsovrfovd  43613  fsovcnvlem  43617  dssmapnvod  43624  ntrk0kbimka  43643  clsk3nimkb  43644  neik0pk1imk0  43651  ntrclsfveq1  43664  ntrclsfveq2  43665  ntrclsfveq  43666  ntrclsss  43667  ntrclsiso  43671  ntrclsk2  43672  ntrclskb  43673  ntrclsk3  43674  ntrclsk13  43675  ntrclsk4  43676  ntrneifv3  43686  ntrneineine0lem  43687  ntrneineine1lem  43688  ntrneifv4  43689  ntrneiel2  43690  ntrneicls00  43693  ntrneicls11  43694  ntrneiiso  43695  ntrneik2  43696  ntrneikb  43698  ntrneixb  43699  ntrneik3  43700  ntrneix3  43701  ntrneik13  43702  ntrneix13  43703  ntrneik4w  43704  clsneiel2  43713  clsneifv3  43714  clsneifv4  43715  neicvgel2  43724  neicvgfv  43725  gneispb  43735  elpwinss  44587  stoweidlem39  45597  stoweidlem50  45608  sge0resrnlem  45961  sge0iunmptlemre  45973  psmeasurelem  46028  psmeasure  46029  isubgrvtxuhgr  47368  isuspgrim0  47388  isuspgrimlem  47390  uhgrimisgrgriclem  47414  ssnn0ssfz  47665  iscnrm3rlem3  48213  iscnrm3rlem8  48218  iscnrm3llem1  48220  iscnrm3llem2  48221  iscnrm3l  48222  pgindlem  48398