Theorem elpwid 4560

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3916  df-pw 4553

This theorem is referenced by:  cofon1  8596  cofon2  8597  fopwdom  9008  ssenen  9074  fival  9306  dffi2  9317  elfiun  9324  tskwe  9853  acndom2  9955  fodomfi2  9961  infpwfien  9963  dfac12lem2  10046  ackbij1lem9  10128  ackbij1lem10  10129  ackbij1lem11  10130  ackbij1lem16  10135  ackbij2lem3  10141  cfss  10166  fin23lem7  10217  fin23lem11  10218  enfin2i  10222  isf32lem8  10261  isf34lem4  10278  isf34lem7  10280  isf34lem6  10281  isfin1-3  10287  fin1a2lem13  10313  ttukeylem6  10415  uzssz  12763  elfzoelz  13569  ackbijnn  15745  incexclem  15753  smuval2  16403  smupvallem  16404  smueqlem  16411  ramub1lem1  16948  ramub1lem2  16949  restid2  17344  mress  17505  mrcuni  17537  mreexexlem4d  17563  mreexexd  17564  mreexdomd  17565  isacs2  17569  acsfn  17575  isdrs2  18222  ipodrsima  18457  isacs3lem  18458  acsfiindd  18469  lagsubg2  19116  ghmqusnsg  19204  ghmquskerlem3  19208  ghmqusker  19209  cntzrcl  19249  sylow1lem2  19521  sylow1lem3  19522  sylow1lem4  19523  sylow2alem2  19540  sylow2a  19541  lsmpropd  19599  lssacs  20910  lssacsex  21091  lbsextlem2  21106  lbsextlem3  21107  lbsextlem4  21108  rhmqusnsg  21232  elocv  21615  ppttop  22932  epttop  22934  clsval2  22975  mretopd  23017  neiss2  23026  neiptopnei  23057  ordtbas  23117  subbascn  23179  discmp  23323  uncmp  23328  conncompconn  23357  1stcfb  23370  2ndcdisj  23381  restnlly  23407  nllyrest  23411  nllyidm  23414  cldllycmp  23420  1stckgenlem  23478  dfac14  23543  xkoccn  23544  txnlly  23562  txkgen  23577  xkopt  23580  xkoco2cn  23583  xkoinjcn  23612  tgqtop  23637  nrmhmph  23719  fbelss  23758  fbssfi  23762  infil  23788  alexsubALTlem3  23974  alexsubALTlem4  23975  ustssxp  24130  trust  24154  utopsnneiplem  24172  blssm  24343  blin2  24354  metustss  24476  metust  24483  psmetutop  24492  restmetu  24495  icccmplem2  24749  cncfrss  24821  cncfrss2  24822  bndth  24894  lebnum  24900  ovolicc2  25460  vitalilem5  25550  i1fd  25619  dvbsss  25840  perfdvf  25841  plybss  26136  wilthlem2  27016  oldf  27808  newf  27809  leftf  27820  rightf  27821  elmade  27822  ssltleft  27825  ssltright  27826  cofsslt  27872  coinitsslt  27873  f1otrg  28859  uhgrss  29053  upgrss  29077  usgrss  29163  eupth2lems  30229  ubthlem1  30861  elpwdifcl  32517  elpwiuncl  32518  ssnnssfz  32781  indf1ofs  32858  pwrssmgc  32992  trsp2cyc  33103  lmhmqusker  33393  rhmquskerlem  33401  esplylem  33598  esplymhp  33600  esplyfv1  33601  esplyfv  33602  exsslsb  33620  zarcmplem  33905  esumval  34070  esumel  34071  gsumesum  34083  esumlub  34084  esumpcvgval  34102  esumcvg  34110  elsigass  34149  ispisys2  34177  sigapildsyslem  34185  sigapildsys  34186  ldgenpisyslem1  34187  ldgenpisys  34190  dynkin  34191  rossspw  34193  srossspw  34200  ddemeas  34260  br2base  34293  sxbrsigalem0  34295  dya2iocucvr  34308  sxbrsigalem2  34310  sxbrsiga  34314  oms0  34321  omssubadd  34324  carsguni  34332  elcarsgss  34333  carsggect  34342  omsmeas  34347  eulerpartlemgvv  34400  coinfliplem  34503  ballotlemfmpn  34519  cvmliftmolem2  35337  cvmlift3lem8  35381  neibastop1  36414  neibastop2lem  36415  neibastop2  36416  filnetlem4  36436  cnambfre  37718  heiborlem3  37863  heiborlem5  37865  heiborlem6  37866  heiborlem10  37870  heibor  37871  mapd1o  41757  sticksstones3  42251  prjcrv0  42741  elrfi  42801  elrfirn  42802  elrfirn2  42803  ismrcd1  42805  istopclsd  42807  mrefg3  42815  aomclem2  43162  lsmfgcl  43181  lmhmfgima  43191  elmnc  43243  fpwfvss  43519  rfovcnvf1od  44111  rfovcnvfvd  44114  fsovrfovd  44116  fsovcnvlem  44120  dssmapnvod  44127  ntrk0kbimka  44146  clsk3nimkb  44147  neik0pk1imk0  44154  ntrclsfveq1  44167  ntrclsfveq2  44168  ntrclsfveq  44169  ntrclsss  44170  ntrclsiso  44174  ntrclsk2  44175  ntrclskb  44176  ntrclsk3  44177  ntrclsk13  44178  ntrclsk4  44179  ntrneifv3  44189  ntrneineine0lem  44190  ntrneineine1lem  44191  ntrneifv4  44192  ntrneiel2  44193  ntrneicls00  44196  ntrneicls11  44197  ntrneiiso  44198  ntrneik2  44199  ntrneikb  44201  ntrneixb  44202  ntrneik3  44203  ntrneix3  44204  ntrneik13  44205  ntrneix13  44206  ntrneik4w  44207  clsneiel2  44216  clsneifv3  44217  clsneifv4  44218  neicvgel2  44227  neicvgfv  44228  gneispb  44238  elpwinss  45160  stoweidlem39  46151  stoweidlem50  46162  sge0resrnlem  46515  sge0iunmptlemre  46527  psmeasurelem  46582  psmeasure  46583  isubgrvtxuhgr  47978  isuspgrim0  48008  isuspgrimlem  48009  uhgrimisgrgriclem  48044  ssnn0ssfz  48463  iscnrm3rlem3  49056  iscnrm3rlem8  49061  iscnrm3llem1  49063  iscnrm3llem2  49064  iscnrm3l  49065  pgindlem  49830