Theorem elpwid 4567

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

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-pw 4560

This theorem is referenced by:  cofon1  8646  cofon2  8647  fopwdom  9061  ssenen  9127  fival  9360  dffi2  9371  elfiun  9378  tskwe  9924  acndom2  10026  fodomfi2  10032  infpwfien  10034  dfac12lem2  10116  ackbij1lem9  10198  ackbij1lem10  10199  ackbij1lem11  10200  ackbij1lem16  10205  ackbij2lem3  10211  cfss  10237  fin23lem7  10288  fin23lem11  10289  enfin2i  10293  isf32lem8  10332  isf34lem4  10349  isf34lem7  10351  isf34lem6  10352  isfin1-3  10358  fin1a2lem13  10384  ttukeylem6  10486  uzssz  12874  elfzoelz  13678  ackbijnn  15872  incexclem  15880  smuval2  16530  smupvallem  16531  smueqlem  16538  ramub1lem1  17076  ramub1lem2  17077  restid2  17473  mress  17635  mrcuni  17667  mreexexlem4d  17693  mreexexd  17694  mreexdomd  17695  isacs2  17699  acsfn  17705  isdrs2  18352  ipodrsima  18587  isacs3lem  18588  acsfiindd  18599  lagsubg2  19256  ghmqusnsg  19343  ghmquskerlem3  19347  ghmqusker  19348  cntzrcl  19388  sylow1lem2  19660  sylow1lem3  19661  sylow1lem4  19662  sylow2alem2  19679  sylow2a  19680  lsmpropd  19738  lssacs  21057  lssacsex  21237  lbsextlem2  21252  lbsextlem3  21253  lbsextlem4  21254  rhmqusnsg  21387  elocv  21778  ppttop  23125  epttop  23127  clsval2  23168  mretopd  23210  neiss2  23219  neiptopnei  23250  ordtbas  23310  subbascn  23372  discmp  23516  uncmp  23521  conncompconn  23550  1stcfb  23563  2ndcdisj  23574  restnlly  23600  nllyrest  23604  nllyidm  23607  cldllycmp  23613  1stckgenlem  23671  dfac14  23736  xkoccn  23737  txnlly  23755  txkgen  23770  xkopt  23773  xkoco2cn  23776  xkoinjcn  23805  tgqtop  23830  nrmhmph  23912  fbelss  23951  fbssfi  23955  infil  23981  alexsubALTlem3  24167  alexsubALTlem4  24168  ustssxp  24323  trust  24347  utopsnneiplem  24365  blssm  24536  blin2  24547  metustss  24669  metust  24676  psmetutop  24685  restmetu  24688  icccmplem2  24942  cncfrss  25011  cncfrss2  25012  bndth  25078  lebnum  25084  ovolicc2  25642  vitalilem5  25732  i1fd  25801  dvbsss  26022  perfdvf  26023  plybss  26312  wilthlem2  27191  oldf  27988  newf  27989  leftf  28006  rightf  28007  elmade  28008  sltsleft  28011  sltsright  28012  cofslts  28069  coinitslts  28070  f1otrg  29129  uhgrss  29323  upgrss  29347  usgrss  29433  eupth2lems  30498  ubthlem1  31131  elpwdifcl  32782  elpwiuncl  32783  ssnnssfz  33044  indf1ofs  33099  pwrssmgc  33233  trsp2cyc  33356  lmhmqusker  33642  rhmquskerlem  33649  esplylem  33873  esplymhp  33875  esplyfv1  33876  esplyfv  33877  esplyfval3  33879  exsslsb  33904  zarcmplem  34188  esumval  34353  esumel  34354  gsumesum  34366  esumlub  34367  esumpcvgval  34385  esumcvg  34393  elsigass  34432  ispisys2  34460  sigapildsyslem  34468  sigapildsys  34469  ldgenpisyslem1  34470  ldgenpisys  34473  dynkin  34474  rossspw  34476  srossspw  34483  ddemeas  34543  br2base  34576  sxbrsigalem0  34578  dya2iocucvr  34591  sxbrsigalem2  34593  sxbrsiga  34597  oms0  34604  omssubadd  34607  carsguni  34615  elcarsgss  34616  carsggect  34625  omsmeas  34630  eulerpartlemgvv  34683  coinfliplem  34786  ballotlemfmpn  34802  cvmliftmolem2  35645  cvmlift3lem8  35689  neibastop1  36732  neibastop2lem  36733  neibastop2  36734  filnetlem4  36754  cnambfre  38179  heiborlem3  38324  heiborlem5  38326  heiborlem6  38327  heiborlem10  38331  heibor  38332  mapd1o  42284  sticksstones3  42777  prjcrv0  43227  elrfi  43287  elrfirn  43288  elrfirn2  43289  ismrcd1  43291  istopclsd  43293  mrefg3  43301  aomclem2  43644  lsmfgcl  43663  lmhmfgima  43673  elmnc  43725  fpwfvss  44000  rfovcnvf1od  44592  rfovcnvfvd  44595  fsovrfovd  44597  fsovcnvlem  44601  dssmapnvod  44608  ntrk0kbimka  44627  clsk3nimkb  44628  neik0pk1imk0  44635  ntrclsfveq1  44648  ntrclsfveq2  44649  ntrclsfveq  44650  ntrclsss  44651  ntrclsiso  44655  ntrclsk2  44656  ntrclskb  44657  ntrclsk3  44658  ntrclsk13  44659  ntrclsk4  44660  ntrneifv3  44670  ntrneineine0lem  44671  ntrneineine1lem  44672  ntrneifv4  44673  ntrneiel2  44674  ntrneicls00  44677  ntrneicls11  44678  ntrneiiso  44679  ntrneik2  44680  ntrneikb  44682  ntrneixb  44683  ntrneik3  44684  ntrneix3  44685  ntrneik13  44686  ntrneix13  44687  ntrneik4w  44688  clsneiel2  44697  clsneifv3  44698  clsneifv4  44699  neicvgel2  44708  neicvgfv  44709  gneispb  44719  elpwinss  45627  stoweidlem39  46611  stoweidlem50  46622  sge0resrnlem  46975  sge0iunmptlemre  46987  psmeasurelem  47042  psmeasure  47043  isubgrvtxuhgr  48484  isuspgrim0  48514  isuspgrimlem  48515  uhgrimisgrgriclem  48550  ssnn0ssfz  48980  iscnrm3rlem3  49571  iscnrm3rlem8  49576  iscnrm3llem1  49578  iscnrm3llem2  49579  iscnrm3l  49580  pgindlem  50344