Theorem elpwid 4611

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3948  𝒫 cpw 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  cofon1  8673  cofon2  8674  fopwdom  9082  ssenen  9153  fival  9409  dffi2  9420  elfiun  9427  tskwe  9947  acndom2  10051  fodomfi2  10057  infpwfien  10059  dfac12lem2  10141  ackbij1lem9  10225  ackbij1lem10  10226  ackbij1lem11  10227  ackbij1lem16  10232  ackbij2lem3  10238  cfss  10262  fin23lem7  10313  fin23lem11  10314  enfin2i  10318  isf32lem8  10357  isf34lem4  10374  isf34lem7  10376  isf34lem6  10377  isfin1-3  10383  fin1a2lem13  10409  ttukeylem6  10511  uzssz  12847  elfzoelz  13636  ackbijnn  15778  incexclem  15786  smuval2  16427  smupvallem  16428  smueqlem  16435  ramub1lem1  16963  ramub1lem2  16964  restid2  17380  mress  17541  mrcuni  17569  mreexexlem4d  17595  mreexexd  17596  mreexdomd  17597  isacs2  17601  acsfn  17607  isdrs2  18263  ipodrsima  18498  isacs3lem  18499  acsfiindd  18510  lagsubg2  19109  cntzrcl  19232  sylow1lem2  19508  sylow1lem3  19509  sylow1lem4  19510  sylow2alem2  19527  sylow2a  19528  lsmpropd  19586  lssacs  20722  lssacsex  20902  lbsextlem2  20917  lbsextlem3  20918  lbsextlem4  20919  elocv  21440  ppttop  22730  epttop  22732  clsval2  22774  mretopd  22816  neiss2  22825  neiptopnei  22856  ordtbas  22916  subbascn  22978  discmp  23122  uncmp  23127  conncompconn  23156  1stcfb  23169  2ndcdisj  23180  restnlly  23206  nllyrest  23210  nllyidm  23213  cldllycmp  23219  1stckgenlem  23277  dfac14  23342  xkoccn  23343  txnlly  23361  txkgen  23376  xkopt  23379  xkoco2cn  23382  xkoinjcn  23411  tgqtop  23436  nrmhmph  23518  fbelss  23557  fbssfi  23561  infil  23587  alexsubALTlem3  23773  alexsubALTlem4  23774  ustssxp  23929  trust  23954  utopsnneiplem  23972  blssm  24144  blin2  24155  metustss  24280  metust  24287  psmetutop  24296  restmetu  24299  icccmplem2  24559  cncfrss  24631  cncfrss2  24632  bndth  24698  lebnum  24704  ovolicc2  25263  vitalilem5  25353  i1fd  25422  dvbsss  25643  perfdvf  25644  plybss  25932  wilthlem2  26797  oldf  27577  newf  27578  leftf  27585  rightf  27586  elmade  27587  ssltleft  27590  ssltright  27591  cofsslt  27631  coinitsslt  27632  f1otrg  28377  uhgrss  28579  upgrss  28603  usgrss  28689  eupth2lems  29746  ubthlem1  30378  elpwdifcl  32019  elpwiuncl  32020  ssnnssfz  32253  pwrssmgc  32425  trsp2cyc  32540  ghmquskerlem3  32793  ghmqusker  32794  lmhmqusker  32796  rhmquskerlem  32805  zarcmplem  33147  indf1ofs  33310  esumval  33330  esumel  33331  gsumesum  33343  esumlub  33344  esumpcvgval  33362  esumcvg  33370  elsigass  33409  ispisys2  33437  sigapildsyslem  33445  sigapildsys  33446  ldgenpisyslem1  33447  ldgenpisys  33450  dynkin  33451  rossspw  33453  srossspw  33460  ddemeas  33520  br2base  33554  sxbrsigalem0  33556  dya2iocucvr  33569  sxbrsigalem2  33571  sxbrsiga  33575  oms0  33582  omssubadd  33585  carsguni  33593  elcarsgss  33594  carsggect  33603  omsmeas  33608  eulerpartlemgvv  33661  coinfliplem  33763  ballotlemfmpn  33779  cvmliftmolem2  34559  cvmlift3lem8  34603  neibastop1  35547  neibastop2lem  35548  neibastop2  35549  filnetlem4  35569  cnambfre  36839  heiborlem3  36984  heiborlem5  36986  heiborlem6  36987  heiborlem10  36991  heibor  36992  mapd1o  40822  sticksstones3  41270  prjcrv0  41677  elrfi  41734  elrfirn  41735  elrfirn2  41736  ismrcd1  41738  istopclsd  41740  mrefg3  41748  aomclem2  42099  lsmfgcl  42118  lmhmfgima  42128  elmnc  42180  fpwfvss  42465  rfovcnvf1od  43057  rfovcnvfvd  43060  fsovrfovd  43062  fsovcnvlem  43066  dssmapnvod  43073  ntrk0kbimka  43092  clsk3nimkb  43093  neik0pk1imk0  43100  ntrclsfveq1  43113  ntrclsfveq2  43114  ntrclsfveq  43115  ntrclsss  43116  ntrclsiso  43120  ntrclsk2  43121  ntrclskb  43122  ntrclsk3  43123  ntrclsk13  43124  ntrclsk4  43125  ntrneifv3  43135  ntrneineine0lem  43136  ntrneineine1lem  43137  ntrneifv4  43138  ntrneiel2  43139  ntrneicls00  43142  ntrneicls11  43143  ntrneiiso  43144  ntrneik2  43145  ntrneikb  43147  ntrneixb  43148  ntrneik3  43149  ntrneix3  43150  ntrneik13  43151  ntrneix13  43152  ntrneik4w  43153  clsneiel2  43162  clsneifv3  43163  clsneifv4  43164  neicvgel2  43173  neicvgfv  43174  gneispb  43184  elpwinss  44038  stoweidlem39  45054  stoweidlem50  45065  sge0resrnlem  45418  sge0iunmptlemre  45430  psmeasurelem  45485  psmeasure  45486  ssnn0ssfz  47114  iscnrm3rlem3  47663  iscnrm3rlem8  47668  iscnrm3llem1  47670  iscnrm3llem2  47671  iscnrm3l  47672  pgindlem  47848