Theorem elpwid 4565

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-pw 4558

This theorem is used by:  cofon1  8683  cofon2  8684  fopwdom  9106  ssenen  9172  fival  9406  dffi2  9417  elfiun  9424  tskwe  10033  acndom2  10135  fodomfi2  10141  infpwfien  10143  dfac12lem2  10225  ackbij1lem9  10307  ackbij1lem10  10308  ackbij1lem11  10309  ackbij1lem16  10314  ackbij2lem3  10320  cfss  10345  fin23lem7  10396  fin23lem11  10397  enfin2i  10401  isf32lem8  10440  isf34lem4  10457  isf34lem7  10459  isf34lem6  10460  isfin1-3  10466  fin1a2lem13  10492  ttukeylem6  10594  uzssz  12988  elfzoelz  13795  ackbijnn  15999  incexclem  16007  smuval2  16654  smupvallem  16655  smueqlem  16662  ramub1lem1  17206  ramub1lem2  17207  restid2  17603  mress  17765  mrcuni  17797  mreexexlem4d  17823  mreexexd  17824  mreexdomd  17825  isacs2  17829  acsfn  17835  isdrs2  18482  ipodrsima  18717  isacs3lem  18718  acsfiindd  18729  lagsubg2  19411  ghmqusnsg  19498  ghmquskerlem3  19502  ghmqusker  19503  cntzrcl  19543  sylow1lem2  19815  sylow1lem3  19816  sylow1lem4  19817  sylow2alem2  19834  sylow2a  19835  lsmpropd  19893  lssacs  21244  lssacsex  21424  lbsextlem2  21439  lbsextlem3  21440  lbsextlem4  21441  rhmqusnsg  21583  elocv  21976  ppttop  23327  epttop  23329  clsval2  23370  mretopd  23412  neiss2  23421  neiptopnei  23452  ordtbas  23512  subbascn  23574  discmp  23718  uncmp  23723  conncompconn  23752  1stcfb  23765  2ndcdisj  23777  restnlly  23803  nllyrest  23807  nllyidm  23810  cldllycmp  23816  1stckgenlem  23874  dfac14  23939  xkoccn  23940  txnlly  23958  txkgen  23973  xkopt  23976  xkoco2cn  23979  xkoinjcn  24008  tgqtop  24033  nrmhmph  24115  fbelss  24154  fbssfi  24158  infil  24184  alexsubALTlem3  24370  alexsubALTlem4  24371  ustssxp  24526  trust  24550  utopsnneiplem  24568  blssm  24739  blin2  24750  metustss  24872  metust  24879  psmetutop  24888  restmetu  24891  icccmplem2  25145  cncfrss  25214  cncfrss2  25215  bndth  25281  lebnum  25287  ovolicc2  25845  vitalilem5  25935  i1fd  26004  dvbsss  26224  perfdvf  26225  plybss  26514  wilthlem2  27398  oldf  28225  newf  28226  leftf  28243  rightf  28244  elmade  28245  sltsleft  28248  sltsright  28249  cofslts  28306  coinitslts  28307  f1otrg  29450  uhgrss  29644  upgrss  29668  usgrss  29757  eupth2lems  30841  ubthlem1  31474  elpwdifcl  33166  elpwiuncl  33167  ssnnssfz  33423  indf1ofs  33477  pwrssmgc  33605  trsp2cyc  33728  lmhmqusker  34012  rhmquskerlem  34019  esplylem  34242  esplymhp  34244  esplyfv1  34245  esplyfv  34246  esplyfval3  34248  exsslsb  34273  zarcmplem  34557  esumval  34722  esumel  34723  gsumesum  34735  esumlub  34736  esumpcvgval  34754  esumcvg  34762  elsigass  34801  ispisys2  34830  sigapildsyslem  34838  sigapildsys  34839  ldgenpisyslem1  34840  ldgenpisys  34843  dynkin  34844  rossspw  34846  srossspw  34853  ddemeas  34913  br2base  34945  sxbrsigalem0  34947  dya2iocucvr  34960  sxbrsigalem2  34962  sxbrsiga  34966  oms0  34973  omssubadd  34976  carsguni  34984  elcarsgss  34985  carsggect  34994  omsmeas  34999  eulerpartlemgvv  35052  coinfliplem  35155  ballotlemfmpn  35171  cvmliftmolem2  36131  cvmlift3lem8  36175  neibastop1  37237  neibastop2lem  37238  neibastop2  37239  filnetlem4  37259  cnambfre  38677  heiborlem3  38838  heiborlem5  38840  heiborlem6  38841  heiborlem10  38845  heibor  38846  mapd1o  42796  sticksstones3  43289  elprjspnss  43741  elrfi  43796  elrfirn  43797  elrfirn2  43798  ismrcd1  43800  istopclsd  43802  mrefg3  43810  aomclem2  44148  lsmfgcl  44167  lmhmfgima  44177  elmnc  44229  fpwfvss  44504  rfovcnvf1od  45095  rfovcnvfvd  45098  fsovrfovd  45100  fsovcnvlem  45104  dssmapnvod  45111  ntrk0kbimka  45130  clsk3nimkb  45131  neik0pk1imk0  45138  ntrclsfveq1  45151  ntrclsfveq2  45152  ntrclsfveq  45153  ntrclsss  45154  ntrclsiso  45158  ntrclsk2  45159  ntrclskb  45160  ntrclsk3  45161  ntrclsk13  45162  ntrclsk4  45163  ntrneifv3  45173  ntrneineine0lem  45174  ntrneineine1lem  45175  ntrneifv4  45176  ntrneiel2  45177  ntrneicls00  45180  ntrneicls11  45181  ntrneiiso  45182  ntrneik2  45183  ntrneikb  45185  ntrneixb  45186  ntrneik3  45187  ntrneix3  45188  ntrneik13  45189  ntrneix13  45190  ntrneik4w  45191  clsneiel2  45200  clsneifv3  45201  clsneifv4  45202  neicvgel2  45211  neicvgfv  45212  gneispb  45222  hfstructfun  46117  rnhfstructsshf  46118  elpwinss  46157  stoweidlem39  47140  stoweidlem50  47151  sge0resrnlem  47504  sge0iunmptlemre  47516  psmeasurelem  47571  psmeasure  47572  tmachlem-agreeprod  48038  tmachlem-exagreecover  48047  isubgrvtxuhgr  49053  isuspgrim0  49083  isuspgrimlem  49084  uhgrimisgrgriclem  49119  ssnn0ssfz  49552  iscnrm3rlem3  50147  iscnrm3rlem8  50152  iscnrm3llem1  50154  iscnrm3llem2  50155  iscnrm3l  50156  parhomss2  50847  parhomss  50848  pgindlem  50974