Theorem elpwid 4576

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3908  𝒫 cpw 4567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-pw 4569

This theorem is used by:  cofon1  8667  cofon2  8668  fopwdom  9083  ssenen  9149  fival  9382  dffi2  9393  elfiun  9400  tskwe  9955  acndom2  10057  fodomfi2  10063  infpwfien  10065  dfac12lem2  10147  ackbij1lem9  10229  ackbij1lem10  10230  ackbij1lem11  10231  ackbij1lem16  10236  ackbij2lem3  10242  cfss  10267  fin23lem7  10318  fin23lem11  10319  enfin2i  10323  isf32lem8  10362  isf34lem4  10379  isf34lem7  10381  isf34lem6  10382  isfin1-3  10388  fin1a2lem13  10414  ttukeylem6  10516  uzssz  12901  elfzoelz  13706  ackbijnn  15908  incexclem  15916  smuval2  16565  smupvallem  16566  smueqlem  16573  ramub1lem1  17111  ramub1lem2  17112  restid2  17508  mress  17670  mrcuni  17702  mreexexlem4d  17728  mreexexd  17729  mreexdomd  17730  isacs2  17734  acsfn  17740  isdrs2  18387  ipodrsima  18622  isacs3lem  18623  acsfiindd  18634  lagsubg2  19290  ghmqusnsg  19377  ghmquskerlem3  19381  ghmqusker  19382  cntzrcl  19422  sylow1lem2  19694  sylow1lem3  19695  sylow1lem4  19696  sylow2alem2  19713  sylow2a  19714  lsmpropd  19772  lssacs  21118  lssacsex  21298  lbsextlem2  21313  lbsextlem3  21314  lbsextlem4  21315  rhmqusnsg  21455  elocv  21848  ppttop  23194  epttop  23196  clsval2  23237  mretopd  23279  neiss2  23288  neiptopnei  23319  ordtbas  23379  subbascn  23441  discmp  23585  uncmp  23590  conncompconn  23619  1stcfb  23632  2ndcdisj  23643  restnlly  23669  nllyrest  23673  nllyidm  23676  cldllycmp  23682  1stckgenlem  23740  dfac14  23805  xkoccn  23806  txnlly  23824  txkgen  23839  xkopt  23842  xkoco2cn  23845  xkoinjcn  23874  tgqtop  23899  nrmhmph  23981  fbelss  24020  fbssfi  24024  infil  24050  alexsubALTlem3  24236  alexsubALTlem4  24237  ustssxp  24392  trust  24416  utopsnneiplem  24434  blssm  24605  blin2  24616  metustss  24738  metust  24745  psmetutop  24754  restmetu  24757  icccmplem2  25011  cncfrss  25080  cncfrss2  25081  bndth  25147  lebnum  25153  ovolicc2  25711  vitalilem5  25801  i1fd  25870  dvbsss  26091  perfdvf  26092  plybss  26381  wilthlem2  27263  oldf  28060  newf  28061  leftf  28078  rightf  28079  elmade  28080  sltsleft  28083  sltsright  28084  cofslts  28141  coinitslts  28142  f1otrg  29250  uhgrss  29444  upgrss  29468  usgrss  29554  eupth2lems  30619  ubthlem1  31252  elpwdifcl  32902  elpwiuncl  32903  ssnnssfz  33162  indf1ofs  33216  pwrssmgc  33344  trsp2cyc  33467  lmhmqusker  33750  rhmquskerlem  33757  esplylem  33980  esplymhp  33982  esplyfv1  33983  esplyfv  33984  esplyfval3  33986  exsslsb  34011  zarcmplem  34295  esumval  34460  esumel  34461  gsumesum  34473  esumlub  34474  esumpcvgval  34492  esumcvg  34500  elsigass  34539  ispisys2  34567  sigapildsyslem  34575  sigapildsys  34576  ldgenpisyslem1  34577  ldgenpisys  34580  dynkin  34581  rossspw  34583  srossspw  34590  ddemeas  34650  br2base  34683  sxbrsigalem0  34685  dya2iocucvr  34698  sxbrsigalem2  34700  sxbrsiga  34704  oms0  34711  omssubadd  34714  carsguni  34722  elcarsgss  34723  carsggect  34732  omsmeas  34737  eulerpartlemgvv  34790  coinfliplem  34893  ballotlemfmpn  34909  cvmliftmolem2  35787  cvmlift3lem8  35831  neibastop1  36903  neibastop2lem  36904  neibastop2  36905  filnetlem4  36925  cnambfre  38352  heiborlem3  38497  heiborlem5  38499  heiborlem6  38500  heiborlem10  38504  heibor  38505  mapd1o  42455  sticksstones3  42948  prjcrv0  43398  elrfi  43458  elrfirn  43459  elrfirn2  43460  ismrcd1  43462  istopclsd  43464  mrefg3  43472  aomclem2  43815  lsmfgcl  43834  lmhmfgima  43844  elmnc  43896  fpwfvss  44171  rfovcnvf1od  44763  rfovcnvfvd  44766  fsovrfovd  44768  fsovcnvlem  44772  dssmapnvod  44779  ntrk0kbimka  44798  clsk3nimkb  44799  neik0pk1imk0  44806  ntrclsfveq1  44819  ntrclsfveq2  44820  ntrclsfveq  44821  ntrclsss  44822  ntrclsiso  44826  ntrclsk2  44827  ntrclskb  44828  ntrclsk3  44829  ntrclsk13  44830  ntrclsk4  44831  ntrneifv3  44841  ntrneineine0lem  44842  ntrneineine1lem  44843  ntrneifv4  44844  ntrneiel2  44845  ntrneicls00  44848  ntrneicls11  44849  ntrneiiso  44850  ntrneik2  44851  ntrneikb  44853  ntrneixb  44854  ntrneik3  44855  ntrneix3  44856  ntrneik13  44857  ntrneix13  44858  ntrneik4w  44859  clsneiel2  44868  clsneifv3  44869  clsneifv4  44870  neicvgel2  44879  neicvgfv  44880  gneispb  44890  elpwinss  45802  stoweidlem39  46786  stoweidlem50  46797  sge0resrnlem  47150  sge0iunmptlemre  47162  psmeasurelem  47217  psmeasure  47218  isubgrvtxuhgr  48662  isuspgrim0  48692  isuspgrimlem  48693  uhgrimisgrgriclem  48728  ssnn0ssfz  49162  iscnrm3rlem3  49753  iscnrm3rlem8  49758  iscnrm3llem1  49760  iscnrm3llem2  49761  iscnrm3l  49762  pgindlem  50526