Theorem elpwid 4570

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-pw 4563

This theorem is referenced by:  cofon1  8657  cofon2  8658  fopwdom  9072  ssenen  9138  fival  9371  dffi2  9382  elfiun  9389  tskwe  9935  acndom2  10037  fodomfi2  10043  infpwfien  10045  dfac12lem2  10127  ackbij1lem9  10209  ackbij1lem10  10210  ackbij1lem11  10211  ackbij1lem16  10216  ackbij2lem3  10222  cfss  10248  fin23lem7  10299  fin23lem11  10300  enfin2i  10304  isf32lem8  10343  isf34lem4  10360  isf34lem7  10362  isf34lem6  10363  isfin1-3  10369  fin1a2lem13  10395  ttukeylem6  10497  uzssz  12882  elfzoelz  13687  ackbijnn  15882  incexclem  15890  smuval2  16539  smupvallem  16540  smueqlem  16547  ramub1lem1  17085  ramub1lem2  17086  restid2  17482  mress  17644  mrcuni  17676  mreexexlem4d  17702  mreexexd  17703  mreexdomd  17704  isacs2  17708  acsfn  17714  isdrs2  18361  ipodrsima  18596  isacs3lem  18597  acsfiindd  18608  lagsubg2  19264  ghmqusnsg  19351  ghmquskerlem3  19355  ghmqusker  19356  cntzrcl  19396  sylow1lem2  19668  sylow1lem3  19669  sylow1lem4  19670  sylow2alem2  19687  sylow2a  19688  lsmpropd  19746  lssacs  21067  lssacsex  21247  lbsextlem2  21262  lbsextlem3  21263  lbsextlem4  21264  rhmqusnsg  21404  elocv  21797  ppttop  23143  epttop  23145  clsval2  23186  mretopd  23228  neiss2  23237  neiptopnei  23268  ordtbas  23328  subbascn  23390  discmp  23534  uncmp  23539  conncompconn  23568  1stcfb  23581  2ndcdisj  23592  restnlly  23618  nllyrest  23622  nllyidm  23625  cldllycmp  23631  1stckgenlem  23689  dfac14  23754  xkoccn  23755  txnlly  23773  txkgen  23788  xkopt  23791  xkoco2cn  23794  xkoinjcn  23823  tgqtop  23848  nrmhmph  23930  fbelss  23969  fbssfi  23973  infil  23999  alexsubALTlem3  24185  alexsubALTlem4  24186  ustssxp  24341  trust  24365  utopsnneiplem  24383  blssm  24554  blin2  24565  metustss  24687  metust  24694  psmetutop  24703  restmetu  24706  icccmplem2  24960  cncfrss  25029  cncfrss2  25030  bndth  25096  lebnum  25102  ovolicc2  25660  vitalilem5  25750  i1fd  25819  dvbsss  26040  perfdvf  26041  plybss  26330  wilthlem2  27209  oldf  28006  newf  28007  leftf  28024  rightf  28025  elmade  28026  sltsleft  28029  sltsright  28030  cofslts  28087  coinitslts  28088  f1otrg  29186  uhgrss  29380  upgrss  29404  usgrss  29490  eupth2lems  30555  ubthlem1  31188  elpwdifcl  32838  elpwiuncl  32839  ssnnssfz  33098  indf1ofs  33152  pwrssmgc  33286  trsp2cyc  33409  lmhmqusker  33692  rhmquskerlem  33699  esplylem  33922  esplymhp  33924  esplyfv1  33925  esplyfv  33926  esplyfval3  33928  exsslsb  33953  zarcmplem  34237  esumval  34402  esumel  34403  gsumesum  34415  esumlub  34416  esumpcvgval  34434  esumcvg  34442  elsigass  34481  ispisys2  34509  sigapildsyslem  34517  sigapildsys  34518  ldgenpisyslem1  34519  ldgenpisys  34522  dynkin  34523  rossspw  34525  srossspw  34532  ddemeas  34592  br2base  34625  sxbrsigalem0  34627  dya2iocucvr  34640  sxbrsigalem2  34642  sxbrsiga  34646  oms0  34653  omssubadd  34656  carsguni  34664  elcarsgss  34665  carsggect  34674  omsmeas  34679  eulerpartlemgvv  34732  coinfliplem  34835  ballotlemfmpn  34851  cvmliftmolem2  35740  cvmlift3lem8  35784  neibastop1  36836  neibastop2lem  36837  neibastop2  36838  filnetlem4  36858  cnambfre  38285  heiborlem3  38430  heiborlem5  38432  heiborlem6  38433  heiborlem10  38437  heibor  38438  mapd1o  42390  sticksstones3  42883  prjcrv0  43335  elrfi  43395  elrfirn  43396  elrfirn2  43397  ismrcd1  43399  istopclsd  43401  mrefg3  43409  aomclem2  43752  lsmfgcl  43771  lmhmfgima  43781  elmnc  43833  fpwfvss  44108  rfovcnvf1od  44700  rfovcnvfvd  44703  fsovrfovd  44705  fsovcnvlem  44709  dssmapnvod  44716  ntrk0kbimka  44735  clsk3nimkb  44736  neik0pk1imk0  44743  ntrclsfveq1  44756  ntrclsfveq2  44757  ntrclsfveq  44758  ntrclsss  44759  ntrclsiso  44763  ntrclsk2  44764  ntrclskb  44765  ntrclsk3  44766  ntrclsk13  44767  ntrclsk4  44768  ntrneifv3  44778  ntrneineine0lem  44779  ntrneineine1lem  44780  ntrneifv4  44781  ntrneiel2  44782  ntrneicls00  44785  ntrneicls11  44786  ntrneiiso  44787  ntrneik2  44788  ntrneikb  44790  ntrneixb  44791  ntrneik3  44792  ntrneix3  44793  ntrneik13  44794  ntrneix13  44795  ntrneik4w  44796  clsneiel2  44805  clsneifv3  44806  clsneifv4  44807  neicvgel2  44816  neicvgfv  44817  gneispb  44827  elpwinss  45739  stoweidlem39  46723  stoweidlem50  46734  sge0resrnlem  47087  sge0iunmptlemre  47099  psmeasurelem  47154  psmeasure  47155  isubgrvtxuhgr  48596  isuspgrim0  48626  isuspgrimlem  48627  uhgrimisgrgriclem  48662  ssnn0ssfz  49096  iscnrm3rlem3  49687  iscnrm3rlem8  49692  iscnrm3llem1  49694  iscnrm3llem2  49695  iscnrm3l  49696  pgindlem  50460