Theorem elpwid 4576

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-pw 4569

This theorem is referenced by:  cofon1  8657  cofon2  8658  fopwdom  9072  ssenen  9138  fival  9371  dffi2  9382  elfiun  9389  tskwe  9935  acndom2  10037  fodomfi2  10043  infpwfien  10045  dfac12lem2  10127  ackbij1lem9  10209  ackbij1lem10  10210  ackbij1lem11  10211  ackbij1lem16  10216  ackbij2lem3  10222  cfss  10248  fin23lem7  10299  fin23lem11  10300  enfin2i  10304  isf32lem8  10343  isf34lem4  10360  isf34lem7  10362  isf34lem6  10363  isfin1-3  10369  fin1a2lem13  10395  ttukeylem6  10497  uzssz  12882  elfzoelz  13686  ackbijnn  15881  incexclem  15889  smuval2  16539  smupvallem  16540  smueqlem  16547  ramub1lem1  17085  ramub1lem2  17086  restid2  17482  mress  17644  mrcuni  17676  mreexexlem4d  17702  mreexexd  17703  mreexdomd  17704  isacs2  17708  acsfn  17714  isdrs2  18361  ipodrsima  18596  isacs3lem  18597  acsfiindd  18608  lagsubg2  19264  ghmqusnsg  19351  ghmquskerlem3  19355  ghmqusker  19356  cntzrcl  19396  sylow1lem2  19668  sylow1lem3  19669  sylow1lem4  19670  sylow2alem2  19687  sylow2a  19688  lsmpropd  19746  lssacs  21065  lssacsex  21245  lbsextlem2  21260  lbsextlem3  21261  lbsextlem4  21262  rhmqusnsg  21395  elocv  21786  ppttop  23132  epttop  23134  clsval2  23175  mretopd  23217  neiss2  23226  neiptopnei  23257  ordtbas  23317  subbascn  23379  discmp  23523  uncmp  23528  conncompconn  23557  1stcfb  23570  2ndcdisj  23581  restnlly  23607  nllyrest  23611  nllyidm  23614  cldllycmp  23620  1stckgenlem  23678  dfac14  23743  xkoccn  23744  txnlly  23762  txkgen  23777  xkopt  23780  xkoco2cn  23783  xkoinjcn  23812  tgqtop  23837  nrmhmph  23919  fbelss  23958  fbssfi  23962  infil  23988  alexsubALTlem3  24174  alexsubALTlem4  24175  ustssxp  24330  trust  24354  utopsnneiplem  24372  blssm  24543  blin2  24554  metustss  24676  metust  24683  psmetutop  24692  restmetu  24695  icccmplem2  24949  cncfrss  25018  cncfrss2  25019  bndth  25085  lebnum  25091  ovolicc2  25649  vitalilem5  25739  i1fd  25808  dvbsss  26029  perfdvf  26030  plybss  26319  wilthlem2  27198  oldf  27995  newf  27996  leftf  28013  rightf  28014  elmade  28015  sltsleft  28018  sltsright  28019  cofslts  28076  coinitslts  28077  f1otrg  29160  uhgrss  29354  upgrss  29378  usgrss  29464  eupth2lems  30529  ubthlem1  31162  elpwdifcl  32812  elpwiuncl  32813  ssnnssfz  33072  indf1ofs  33126  pwrssmgc  33260  trsp2cyc  33383  lmhmqusker  33669  rhmquskerlem  33676  esplylem  33900  esplymhp  33902  esplyfv1  33903  esplyfv  33904  esplyfval3  33906  exsslsb  33931  zarcmplem  34215  esumval  34380  esumel  34381  gsumesum  34393  esumlub  34394  esumpcvgval  34412  esumcvg  34420  elsigass  34459  ispisys2  34487  sigapildsyslem  34495  sigapildsys  34496  ldgenpisyslem1  34497  ldgenpisys  34500  dynkin  34501  rossspw  34503  srossspw  34510  ddemeas  34570  br2base  34603  sxbrsigalem0  34605  dya2iocucvr  34618  sxbrsigalem2  34620  sxbrsiga  34624  oms0  34631  omssubadd  34634  carsguni  34642  elcarsgss  34643  carsggect  34652  omsmeas  34657  eulerpartlemgvv  34710  coinfliplem  34813  ballotlemfmpn  34829  cvmliftmolem2  35672  cvmlift3lem8  35716  neibastop1  36758  neibastop2lem  36759  neibastop2  36760  filnetlem4  36780  cnambfre  38206  heiborlem3  38351  heiborlem5  38353  heiborlem6  38354  heiborlem10  38358  heibor  38359  mapd1o  42311  sticksstones3  42804  prjcrv0  43256  elrfi  43316  elrfirn  43317  elrfirn2  43318  ismrcd1  43320  istopclsd  43322  mrefg3  43330  aomclem2  43673  lsmfgcl  43692  lmhmfgima  43702  elmnc  43754  fpwfvss  44029  rfovcnvf1od  44621  rfovcnvfvd  44624  fsovrfovd  44626  fsovcnvlem  44630  dssmapnvod  44637  ntrk0kbimka  44656  clsk3nimkb  44657  neik0pk1imk0  44664  ntrclsfveq1  44677  ntrclsfveq2  44678  ntrclsfveq  44679  ntrclsss  44680  ntrclsiso  44684  ntrclsk2  44685  ntrclskb  44686  ntrclsk3  44687  ntrclsk13  44688  ntrclsk4  44689  ntrneifv3  44699  ntrneineine0lem  44700  ntrneineine1lem  44701  ntrneifv4  44702  ntrneiel2  44703  ntrneicls00  44706  ntrneicls11  44707  ntrneiiso  44708  ntrneik2  44709  ntrneikb  44711  ntrneixb  44712  ntrneik3  44713  ntrneix3  44714  ntrneik13  44715  ntrneix13  44716  ntrneik4w  44717  clsneiel2  44726  clsneifv3  44727  clsneifv4  44728  neicvgel2  44737  neicvgfv  44738  gneispb  44748  elpwinss  45660  stoweidlem39  46644  stoweidlem50  46655  sge0resrnlem  47008  sge0iunmptlemre  47020  psmeasurelem  47075  psmeasure  47076  isubgrvtxuhgr  48517  isuspgrim0  48547  isuspgrimlem  48548  uhgrimisgrgriclem  48583  ssnn0ssfz  49013  iscnrm3rlem3  49604  iscnrm3rlem8  49609  iscnrm3llem1  49611  iscnrm3llem2  49612  iscnrm3l  49613  pgindlem  50377