Theorem elpwid 4563

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-pw 4556

This theorem is referenced by:  cofon1  8635  cofon2  8636  fopwdom  9051  ssenen  9117  fival  9353  dffi2  9364  elfiun  9371  tskwe  9903  acndom2  10005  fodomfi2  10011  infpwfien  10013  dfac12lem2  10096  ackbij1lem9  10178  ackbij1lem10  10179  ackbij1lem11  10180  ackbij1lem16  10185  ackbij2lem3  10191  cfss  10217  fin23lem7  10268  fin23lem11  10269  enfin2i  10273  isf32lem8  10312  isf34lem4  10329  isf34lem7  10331  isf34lem6  10332  isfin1-3  10338  fin1a2lem13  10364  ttukeylem6  10466  uzssz  12855  elfzoelz  13659  ackbijnn  15839  incexclem  15847  smuval2  16497  smupvallem  16498  smueqlem  16505  ramub1lem1  17043  ramub1lem2  17044  restid2  17440  mress  17602  mrcuni  17634  mreexexlem4d  17660  mreexexd  17661  mreexdomd  17662  isacs2  17666  acsfn  17672  isdrs2  18319  ipodrsima  18554  isacs3lem  18555  acsfiindd  18566  lagsubg2  19216  ghmqusnsg  19303  ghmquskerlem3  19307  ghmqusker  19308  cntzrcl  19348  sylow1lem2  19620  sylow1lem3  19621  sylow1lem4  19622  sylow2alem2  19639  sylow2a  19640  lsmpropd  19698  lssacs  21012  lssacsex  21192  lbsextlem2  21207  lbsextlem3  21208  lbsextlem4  21209  rhmqusnsg  21333  elocv  21698  ppttop  23045  epttop  23047  clsval2  23088  mretopd  23130  neiss2  23139  neiptopnei  23170  ordtbas  23230  subbascn  23292  discmp  23436  uncmp  23441  conncompconn  23470  1stcfb  23483  2ndcdisj  23494  restnlly  23520  nllyrest  23524  nllyidm  23527  cldllycmp  23533  1stckgenlem  23591  dfac14  23656  xkoccn  23657  txnlly  23675  txkgen  23690  xkopt  23693  xkoco2cn  23696  xkoinjcn  23725  tgqtop  23750  nrmhmph  23832  fbelss  23871  fbssfi  23875  infil  23901  alexsubALTlem3  24087  alexsubALTlem4  24088  ustssxp  24243  trust  24267  utopsnneiplem  24285  blssm  24456  blin2  24467  metustss  24589  metust  24596  psmetutop  24605  restmetu  24608  icccmplem2  24862  cncfrss  24931  cncfrss2  24932  bndth  24998  lebnum  25004  ovolicc2  25562  vitalilem5  25652  i1fd  25721  dvbsss  25942  perfdvf  25943  plybss  26232  wilthlem2  27108  oldf  27905  newf  27906  leftf  27923  rightf  27924  elmade  27925  sltsleft  27928  sltsright  27929  cofslts  27986  coinitslts  27987  f1otrg  29015  uhgrss  29209  upgrss  29233  usgrss  29319  eupth2lems  30384  ubthlem1  31017  elpwdifcl  32672  elpwiuncl  32673  ssnnssfz  32937  indf1ofs  33003  pwrssmgc  33137  trsp2cyc  33262  lmhmqusker  33562  rhmquskerlem  33570  esplylem  33822  esplymhp  33824  esplyfv1  33825  esplyfv  33826  esplyfval3  33828  exsslsb  33853  zarcmplem  34137  esumval  34302  esumel  34303  gsumesum  34315  esumlub  34316  esumpcvgval  34334  esumcvg  34342  elsigass  34381  ispisys2  34409  sigapildsyslem  34417  sigapildsys  34418  ldgenpisyslem1  34419  ldgenpisys  34422  dynkin  34423  rossspw  34425  srossspw  34432  ddemeas  34492  br2base  34525  sxbrsigalem0  34527  dya2iocucvr  34540  sxbrsigalem2  34542  sxbrsiga  34546  oms0  34553  omssubadd  34556  carsguni  34564  elcarsgss  34565  carsggect  34574  omsmeas  34579  eulerpartlemgvv  34632  coinfliplem  34735  ballotlemfmpn  34751  cvmliftmolem2  35585  cvmlift3lem8  35629  neibastop1  36672  neibastop2lem  36673  neibastop2  36674  filnetlem4  36694  cnambfre  38120  heiborlem3  38265  heiborlem5  38267  heiborlem6  38268  heiborlem10  38272  heibor  38273  mapd1o  42225  sticksstones3  42718  prjcrv0  43168  elrfi  43228  elrfirn  43229  elrfirn2  43230  ismrcd1  43232  istopclsd  43234  mrefg3  43242  aomclem2  43585  lsmfgcl  43604  lmhmfgima  43614  elmnc  43666  fpwfvss  43941  rfovcnvf1od  44533  rfovcnvfvd  44536  fsovrfovd  44538  fsovcnvlem  44542  dssmapnvod  44549  ntrk0kbimka  44568  clsk3nimkb  44569  neik0pk1imk0  44576  ntrclsfveq1  44589  ntrclsfveq2  44590  ntrclsfveq  44591  ntrclsss  44592  ntrclsiso  44596  ntrclsk2  44597  ntrclskb  44598  ntrclsk3  44599  ntrclsk13  44600  ntrclsk4  44601  ntrneifv3  44611  ntrneineine0lem  44612  ntrneineine1lem  44613  ntrneifv4  44614  ntrneiel2  44615  ntrneicls00  44618  ntrneicls11  44619  ntrneiiso  44620  ntrneik2  44621  ntrneikb  44623  ntrneixb  44624  ntrneik3  44625  ntrneix3  44626  ntrneik13  44627  ntrneix13  44628  ntrneik4w  44629  clsneiel2  44638  clsneifv3  44639  clsneifv4  44640  neicvgel2  44649  neicvgfv  44650  gneispb  44660  elpwinss  45582  stoweidlem39  46566  stoweidlem50  46577  sge0resrnlem  46930  sge0iunmptlemre  46942  psmeasurelem  46997  psmeasure  46998  isubgrvtxuhgr  48439  isuspgrim0  48469  isuspgrimlem  48470  uhgrimisgrgriclem  48505  ssnn0ssfz  48924  iscnrm3rlem3  49516  iscnrm3rlem8  49521  iscnrm3llem1  49523  iscnrm3llem2  49524  iscnrm3l  49525  pgindlem  50289