Theorem elpwid 4545

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  cofon1  8605  cofon2  8606  fopwdom  9020  ssenen  9086  fival  9322  dffi2  9333  elfiun  9340  tskwe  9872  acndom2  9974  fodomfi2  9980  infpwfien  9982  dfac12lem2  10065  ackbij1lem9  10147  ackbij1lem10  10148  ackbij1lem11  10149  ackbij1lem16  10154  ackbij2lem3  10160  cfss  10185  fin23lem7  10236  fin23lem11  10237  enfin2i  10241  isf32lem8  10280  isf34lem4  10297  isf34lem7  10299  isf34lem6  10300  isfin1-3  10306  fin1a2lem13  10332  ttukeylem6  10434  uzssz  12807  elfzoelz  13611  ackbijnn  15791  incexclem  15799  smuval2  16449  smupvallem  16450  smueqlem  16457  ramub1lem1  16995  ramub1lem2  16996  restid2  17391  mress  17553  mrcuni  17585  mreexexlem4d  17611  mreexexd  17612  mreexdomd  17613  isacs2  17617  acsfn  17623  isdrs2  18270  ipodrsima  18505  isacs3lem  18506  acsfiindd  18517  lagsubg2  19167  ghmqusnsg  19255  ghmquskerlem3  19259  ghmqusker  19260  cntzrcl  19300  sylow1lem2  19572  sylow1lem3  19573  sylow1lem4  19574  sylow2alem2  19591  sylow2a  19592  lsmpropd  19650  lssacs  20964  lssacsex  21144  lbsextlem2  21159  lbsextlem3  21160  lbsextlem4  21161  rhmqusnsg  21285  elocv  21650  ppttop  22997  epttop  22999  clsval2  23040  mretopd  23082  neiss2  23091  neiptopnei  23122  ordtbas  23182  subbascn  23244  discmp  23388  uncmp  23393  conncompconn  23422  1stcfb  23435  2ndcdisj  23446  restnlly  23472  nllyrest  23476  nllyidm  23479  cldllycmp  23485  1stckgenlem  23543  dfac14  23608  xkoccn  23609  txnlly  23627  txkgen  23642  xkopt  23645  xkoco2cn  23648  xkoinjcn  23677  tgqtop  23702  nrmhmph  23784  fbelss  23823  fbssfi  23827  infil  23853  alexsubALTlem3  24039  alexsubALTlem4  24040  ustssxp  24195  trust  24219  utopsnneiplem  24237  blssm  24408  blin2  24419  metustss  24541  metust  24548  psmetutop  24557  restmetu  24560  icccmplem2  24814  cncfrss  24883  cncfrss2  24884  bndth  24950  lebnum  24956  ovolicc2  25514  vitalilem5  25604  i1fd  25673  dvbsss  25894  perfdvf  25895  plybss  26184  wilthlem2  27057  oldf  27854  newf  27855  leftf  27872  rightf  27873  elmade  27874  sltsleft  27877  sltsright  27878  cofslts  27935  coinitslts  27936  f1otrg  28964  uhgrss  29158  upgrss  29182  usgrss  29268  eupth2lems  30333  ubthlem1  30966  elpwdifcl  32621  elpwiuncl  32622  ssnnssfz  32886  indf1ofs  32952  pwrssmgc  33086  trsp2cyc  33211  lmhmqusker  33507  rhmquskerlem  33515  esplylem  33757  esplymhp  33759  esplyfv1  33760  esplyfv  33761  esplyfval3  33763  exsslsb  33788  zarcmplem  34072  esumval  34237  esumel  34238  gsumesum  34250  esumlub  34251  esumpcvgval  34269  esumcvg  34277  elsigass  34316  ispisys2  34344  sigapildsyslem  34352  sigapildsys  34353  ldgenpisyslem1  34354  ldgenpisys  34357  dynkin  34358  rossspw  34360  srossspw  34367  ddemeas  34427  br2base  34460  sxbrsigalem0  34462  dya2iocucvr  34475  sxbrsigalem2  34477  sxbrsiga  34481  oms0  34488  omssubadd  34491  carsguni  34499  elcarsgss  34500  carsggect  34509  omsmeas  34514  eulerpartlemgvv  34567  coinfliplem  34670  ballotlemfmpn  34686  cvmliftmolem2  35511  cvmlift3lem8  35555  neibastop1  36588  neibastop2lem  36589  neibastop2  36590  filnetlem4  36610  cnambfre  38036  heiborlem3  38181  heiborlem5  38183  heiborlem6  38184  heiborlem10  38188  heibor  38189  mapd1o  42141  sticksstones3  42634  prjcrv0  43084  elrfi  43144  elrfirn  43145  elrfirn2  43146  ismrcd1  43148  istopclsd  43150  mrefg3  43158  aomclem2  43501  lsmfgcl  43520  lmhmfgima  43530  elmnc  43582  fpwfvss  43857  rfovcnvf1od  44449  rfovcnvfvd  44452  fsovrfovd  44454  fsovcnvlem  44458  dssmapnvod  44465  ntrk0kbimka  44484  clsk3nimkb  44485  neik0pk1imk0  44492  ntrclsfveq1  44505  ntrclsfveq2  44506  ntrclsfveq  44507  ntrclsss  44508  ntrclsiso  44512  ntrclsk2  44513  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrclsk4  44517  ntrneifv3  44527  ntrneineine0lem  44528  ntrneineine1lem  44529  ntrneifv4  44530  ntrneiel2  44531  ntrneicls00  44534  ntrneicls11  44535  ntrneiiso  44536  ntrneik2  44537  ntrneikb  44539  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  ntrneik4w  44545  clsneiel2  44554  clsneifv3  44555  clsneifv4  44556  neicvgel2  44565  neicvgfv  44566  gneispb  44576  elpwinss  45498  stoweidlem39  46483  stoweidlem50  46494  sge0resrnlem  46847  sge0iunmptlemre  46859  psmeasurelem  46914  psmeasure  46915  isubgrvtxuhgr  48356  isuspgrim0  48386  isuspgrimlem  48387  uhgrimisgrgriclem  48422  ssnn0ssfz  48841  iscnrm3rlem3  49433  iscnrm3rlem8  49438  iscnrm3llem1  49440  iscnrm3llem2  49441  iscnrm3l  49442  pgindlem  50206