Theorem elpwid 4584

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-pw 4577

This theorem is referenced by:  cofon1  8682  cofon2  8683  fopwdom  9092  ssenen  9163  fival  9422  dffi2  9433  elfiun  9440  tskwe  9962  acndom2  10066  fodomfi2  10072  infpwfien  10074  dfac12lem2  10157  ackbij1lem9  10239  ackbij1lem10  10240  ackbij1lem11  10241  ackbij1lem16  10246  ackbij2lem3  10252  cfss  10277  fin23lem7  10328  fin23lem11  10329  enfin2i  10333  isf32lem8  10372  isf34lem4  10389  isf34lem7  10391  isf34lem6  10392  isfin1-3  10398  fin1a2lem13  10424  ttukeylem6  10526  uzssz  12871  elfzoelz  13674  ackbijnn  15842  incexclem  15850  smuval2  16499  smupvallem  16500  smueqlem  16507  ramub1lem1  17044  ramub1lem2  17045  restid2  17442  mress  17603  mrcuni  17631  mreexexlem4d  17657  mreexexd  17658  mreexdomd  17659  isacs2  17663  acsfn  17669  isdrs2  18316  ipodrsima  18549  isacs3lem  18550  acsfiindd  18561  lagsubg2  19175  ghmqusnsg  19263  ghmquskerlem3  19267  ghmqusker  19268  cntzrcl  19308  sylow1lem2  19578  sylow1lem3  19579  sylow1lem4  19580  sylow2alem2  19597  sylow2a  19598  lsmpropd  19656  lssacs  20922  lssacsex  21103  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  rhmqusnsg  21244  elocv  21626  ppttop  22943  epttop  22945  clsval2  22986  mretopd  23028  neiss2  23037  neiptopnei  23068  ordtbas  23128  subbascn  23190  discmp  23334  uncmp  23339  conncompconn  23368  1stcfb  23381  2ndcdisj  23392  restnlly  23418  nllyrest  23422  nllyidm  23425  cldllycmp  23431  1stckgenlem  23489  dfac14  23554  xkoccn  23555  txnlly  23573  txkgen  23588  xkopt  23591  xkoco2cn  23594  xkoinjcn  23623  tgqtop  23648  nrmhmph  23730  fbelss  23769  fbssfi  23773  infil  23799  alexsubALTlem3  23985  alexsubALTlem4  23986  ustssxp  24141  trust  24166  utopsnneiplem  24184  blssm  24355  blin2  24366  metustss  24488  metust  24495  psmetutop  24504  restmetu  24507  icccmplem2  24761  cncfrss  24833  cncfrss2  24834  bndth  24906  lebnum  24912  ovolicc2  25473  vitalilem5  25563  i1fd  25632  dvbsss  25853  perfdvf  25854  plybss  26149  wilthlem2  27029  oldf  27813  newf  27814  leftf  27821  rightf  27822  elmade  27823  ssltleft  27826  ssltright  27827  cofsslt  27869  coinitsslt  27870  f1otrg  28796  uhgrss  28989  upgrss  29013  usgrss  29099  eupth2lems  30165  ubthlem1  30797  elpwdifcl  32453  elpwiuncl  32454  ssnnssfz  32710  indf1ofs  32789  pwrssmgc  32926  trsp2cyc  33080  lmhmqusker  33378  rhmquskerlem  33386  exsslsb  33582  zarcmplem  33858  esumval  34023  esumel  34024  gsumesum  34036  esumlub  34037  esumpcvgval  34055  esumcvg  34063  elsigass  34102  ispisys2  34130  sigapildsyslem  34138  sigapildsys  34139  ldgenpisyslem1  34140  ldgenpisys  34143  dynkin  34144  rossspw  34146  srossspw  34153  ddemeas  34213  br2base  34247  sxbrsigalem0  34249  dya2iocucvr  34262  sxbrsigalem2  34264  sxbrsiga  34268  oms0  34275  omssubadd  34278  carsguni  34286  elcarsgss  34287  carsggect  34296  omsmeas  34301  eulerpartlemgvv  34354  coinfliplem  34457  ballotlemfmpn  34473  cvmliftmolem2  35250  cvmlift3lem8  35294  neibastop1  36323  neibastop2lem  36324  neibastop2  36325  filnetlem4  36345  cnambfre  37638  heiborlem3  37783  heiborlem5  37785  heiborlem6  37786  heiborlem10  37790  heibor  37791  mapd1o  41613  sticksstones3  42107  prjcrv0  42603  elrfi  42664  elrfirn  42665  elrfirn2  42666  ismrcd1  42668  istopclsd  42670  mrefg3  42678  aomclem2  43026  lsmfgcl  43045  lmhmfgima  43055  elmnc  43107  fpwfvss  43383  rfovcnvf1od  43975  rfovcnvfvd  43978  fsovrfovd  43980  fsovcnvlem  43984  dssmapnvod  43991  ntrk0kbimka  44010  clsk3nimkb  44011  neik0pk1imk0  44018  ntrclsfveq1  44031  ntrclsfveq2  44032  ntrclsfveq  44033  ntrclsss  44034  ntrclsiso  44038  ntrclsk2  44039  ntrclskb  44040  ntrclsk3  44041  ntrclsk13  44042  ntrclsk4  44043  ntrneifv3  44053  ntrneineine0lem  44054  ntrneineine1lem  44055  ntrneifv4  44056  ntrneiel2  44057  ntrneicls00  44060  ntrneicls11  44061  ntrneiiso  44062  ntrneik2  44063  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  ntrneik4w  44071  clsneiel2  44080  clsneifv3  44081  clsneifv4  44082  neicvgel2  44091  neicvgfv  44092  gneispb  44102  elpwinss  45021  stoweidlem39  46016  stoweidlem50  46027  sge0resrnlem  46380  sge0iunmptlemre  46392  psmeasurelem  46447  psmeasure  46448  isubgrvtxuhgr  47825  isuspgrim0  47855  isuspgrimlem  47856  uhgrimisgrgriclem  47891  ssnn0ssfz  48272  iscnrm3rlem3  48864  iscnrm3rlem8  48869  iscnrm3llem1  48871  iscnrm3llem2  48872  iscnrm3l  48873  pgindlem  49527