Theorem elpwid 4550

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3892  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-pw 4541

This theorem is referenced by:  fopwdom  8858  ssenen  8929  fival  9159  dffi2  9170  elfiun  9177  tskwe  9719  acndom2  9821  fodomfi2  9827  infpwfien  9829  dfac12lem2  9911  ackbij1lem9  9995  ackbij1lem10  9996  ackbij1lem11  9997  ackbij1lem16  10002  ackbij2lem3  10008  cfss  10032  fin23lem7  10083  fin23lem11  10084  enfin2i  10088  isf32lem8  10127  isf34lem4  10144  isf34lem7  10146  isf34lem6  10147  isfin1-3  10153  fin1a2lem13  10179  ttukeylem6  10281  uzssz  12614  elfzoelz  13398  ackbijnn  15551  incexclem  15559  smuval2  16200  smupvallem  16201  smueqlem  16208  ramub1lem1  16738  ramub1lem2  16739  restid2  17152  mress  17313  mrcuni  17341  mreexexlem4d  17367  mreexexd  17368  mreexdomd  17369  isacs2  17373  acsfn  17379  isdrs2  18035  ipodrsima  18270  isacs3lem  18271  acsfiindd  18282  lagsubg2  18828  cntzrcl  18944  sylow1lem2  19215  sylow1lem3  19216  sylow1lem4  19217  sylow2alem2  19234  sylow2a  19235  lsmpropd  19294  lssacs  20240  lssacsex  20417  lbsextlem2  20432  lbsextlem3  20433  lbsextlem4  20434  elocv  20884  ppttop  22168  epttop  22170  clsval2  22212  mretopd  22254  neiss2  22263  neiptopnei  22294  ordtbas  22354  subbascn  22416  discmp  22560  uncmp  22565  conncompconn  22594  1stcfb  22607  2ndcdisj  22618  restnlly  22644  nllyrest  22648  nllyidm  22651  cldllycmp  22657  1stckgenlem  22715  dfac14  22780  xkoccn  22781  txnlly  22799  txkgen  22814  xkopt  22817  xkoco2cn  22820  xkoinjcn  22849  tgqtop  22874  nrmhmph  22956  fbelss  22995  fbssfi  22999  infil  23025  alexsubALTlem3  23211  alexsubALTlem4  23212  ustssxp  23367  trust  23392  utopsnneiplem  23410  blssm  23582  blin2  23593  metustss  23718  metust  23725  psmetutop  23734  restmetu  23737  icccmplem2  23997  cncfrss  24065  cncfrss2  24066  bndth  24132  lebnum  24138  ovolicc2  24697  vitalilem5  24787  i1fd  24856  dvbsss  25077  perfdvf  25078  plybss  25366  wilthlem2  26229  f1otrg  27243  uhgrss  27445  upgrss  27469  usgrss  27555  eupth2lems  28611  ubthlem1  29241  elpwdifcl  30884  elpwiuncl  30885  ssnnssfz  31117  pwrssmgc  31287  trsp2cyc  31399  zarcmplem  31840  indf1ofs  32003  esumval  32023  esumel  32024  gsumesum  32036  esumlub  32037  esumpcvgval  32055  esumcvg  32063  elsigass  32102  ispisys2  32130  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  ldgenpisys  32143  dynkin  32144  rossspw  32146  srossspw  32153  ddemeas  32213  br2base  32245  sxbrsigalem0  32247  dya2iocucvr  32260  sxbrsigalem2  32262  sxbrsiga  32266  oms0  32273  omssubadd  32276  carsguni  32284  elcarsgss  32285  carsggect  32294  omsmeas  32299  eulerpartlemgvv  32352  coinfliplem  32454  ballotlemfmpn  32470  cvmliftmolem2  33253  cvmlift3lem8  33297  oldf  34050  newf  34051  leftf  34058  rightf  34059  elmade  34060  ssltleft  34063  ssltright  34064  cofsslt  34097  coinitsslt  34098  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  filnetlem4  34579  cnambfre  35834  heiborlem3  35980  heiborlem5  35982  heiborlem6  35983  heiborlem10  35987  heibor  35988  mapd1o  39671  sticksstones3  40113  elrfi  40525  elrfirn  40526  elrfirn2  40527  ismrcd1  40529  istopclsd  40531  mrefg3  40539  aomclem2  40889  lsmfgcl  40908  lmhmfgima  40918  elmnc  40970  rfovcnvf1od  41594  rfovcnvfvd  41597  fsovrfovd  41599  fsovcnvlem  41603  dssmapnvod  41610  ntrk0kbimka  41631  clsk3nimkb  41632  neik0pk1imk0  41639  ntrclsfveq1  41652  ntrclsfveq2  41653  ntrclsfveq  41654  ntrclsss  41655  ntrclsiso  41659  ntrclsk2  41660  ntrclskb  41661  ntrclsk3  41662  ntrclsk13  41663  ntrclsk4  41664  ntrneifv3  41674  ntrneineine0lem  41675  ntrneineine1lem  41676  ntrneifv4  41677  ntrneiel2  41678  ntrneicls00  41681  ntrneicls11  41682  ntrneiiso  41683  ntrneik2  41684  ntrneikb  41686  ntrneixb  41687  ntrneik3  41688  ntrneix3  41689  ntrneik13  41690  ntrneix13  41691  ntrneik4w  41692  clsneiel2  41701  clsneifv3  41702  clsneifv4  41703  neicvgel2  41712  neicvgfv  41713  gneispb  41723  elpwinss  42579  stoweidlem39  43562  stoweidlem50  43573  sge0resrnlem  43923  sge0iunmptlemre  43935  psmeasurelem  43990  psmeasure  43991  ssnn0ssfz  45664  iscnrm3rlem3  46215  iscnrm3rlem8  46220  iscnrm3llem1  46222  iscnrm3llem2  46223  iscnrm3l  46224