Theorem elpwid 4550

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  fopwdom  8625  ssenen  8691  fival  8876  dffi2  8887  elfiun  8894  tskwe  9379  acndom2  9480  fodomfi2  9486  infpwfien  9488  dfac12lem2  9570  ackbij1lem9  9650  ackbij1lem10  9651  ackbij1lem11  9652  ackbij1lem16  9657  ackbij2lem3  9663  cfss  9687  fin23lem7  9738  fin23lem11  9739  enfin2i  9743  isf32lem8  9782  isf34lem4  9799  isf34lem7  9801  isf34lem6  9802  isfin1-3  9808  fin1a2lem13  9834  ttukeylem6  9936  uzssz  12265  elfzoelz  13039  ackbijnn  15183  incexclem  15191  smuval2  15831  smupvallem  15832  smueqlem  15839  ramub1lem1  16362  ramub1lem2  16363  restid2  16704  mress  16864  mrcuni  16892  mreexexlem4d  16918  mreexexd  16919  mreexdomd  16920  isacs2  16924  acsfn  16930  isdrs2  17549  ipodrsima  17775  isacs3lem  17776  acsfiindd  17787  lagsubg2  18341  cntzrcl  18457  sylow1lem2  18724  sylow1lem3  18725  sylow1lem4  18726  sylow2alem2  18743  sylow2a  18744  lsmpropd  18803  lssacs  19739  lssacsex  19916  lbsextlem2  19931  lbsextlem3  19932  lbsextlem4  19933  elocv  20812  ppttop  21615  epttop  21617  clsval2  21658  mretopd  21700  neiss2  21709  neiptopnei  21740  ordtbas  21800  subbascn  21862  discmp  22006  uncmp  22011  conncompconn  22040  1stcfb  22053  2ndcdisj  22064  restnlly  22090  nllyrest  22094  nllyidm  22097  cldllycmp  22103  1stckgenlem  22161  dfac14  22226  xkoccn  22227  txnlly  22245  txkgen  22260  xkopt  22263  xkoco2cn  22266  xkoinjcn  22295  tgqtop  22320  nrmhmph  22402  fbelss  22441  fbssfi  22445  infil  22471  alexsubALTlem3  22657  alexsubALTlem4  22658  ustssxp  22813  trust  22838  utopsnneiplem  22856  blssm  23028  blin2  23039  metustss  23161  metust  23168  psmetutop  23177  restmetu  23180  icccmplem2  23431  cncfrss  23499  cncfrss2  23500  bndth  23562  lebnum  23568  ovolicc2  24123  vitalilem5  24213  i1fd  24282  dvbsss  24500  perfdvf  24501  plybss  24784  wilthlem2  25646  f1otrg  26657  uhgrss  26849  upgrss  26873  usgrss  26959  eupth2lems  28017  ubthlem1  28647  elpwdifcl  30287  elpwiuncl  30288  ssnnssfz  30510  trsp2cyc  30765  indf1ofs  31285  esumval  31305  esumel  31306  gsumesum  31318  esumlub  31319  esumpcvgval  31337  esumcvg  31345  elsigass  31384  ispisys2  31412  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  ldgenpisys  31425  dynkin  31426  rossspw  31428  srossspw  31435  ddemeas  31495  br2base  31527  sxbrsigalem0  31529  dya2iocucvr  31542  sxbrsigalem2  31544  sxbrsiga  31548  oms0  31555  omssubadd  31558  carsguni  31566  elcarsgss  31567  carsggect  31576  omsmeas  31581  eulerpartlemgvv  31634  coinfliplem  31736  ballotlemfmpn  31752  cvmliftmolem2  32529  cvmlift3lem8  32573  neibastop1  33707  neibastop2lem  33708  neibastop2  33709  filnetlem4  33729  cnambfre  34955  heiborlem3  35106  heiborlem5  35108  heiborlem6  35109  heiborlem10  35113  heibor  35114  mapd1o  38799  elrfi  39311  elrfirn  39312  elrfirn2  39313  ismrcd1  39315  istopclsd  39317  mrefg3  39325  aomclem2  39675  lsmfgcl  39694  lmhmfgima  39704  elmnc  39756  rfovcnvf1od  40370  rfovcnvfvd  40373  fsovrfovd  40375  fsovcnvlem  40379  dssmapnvod  40386  ntrk0kbimka  40409  clsk3nimkb  40410  neik0pk1imk0  40417  ntrclsfveq1  40430  ntrclsfveq2  40431  ntrclsfveq  40432  ntrclsss  40433  ntrclsiso  40437  ntrclsk2  40438  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  ntrclsk4  40442  ntrneifv3  40452  ntrneineine0lem  40453  ntrneineine1lem  40454  ntrneifv4  40455  ntrneiel2  40456  ntrneicls00  40459  ntrneicls11  40460  ntrneiiso  40461  ntrneik2  40462  ntrneikb  40464  ntrneixb  40465  ntrneik3  40466  ntrneix3  40467  ntrneik13  40468  ntrneix13  40469  ntrneik4w  40470  clsneiel2  40479  clsneifv3  40480  clsneifv4  40481  neicvgel2  40490  neicvgfv  40491  gneispb  40501  elpwinss  41331  stoweidlem39  42344  stoweidlem50  42355  sge0resrnlem  42705  sge0iunmptlemre  42717  psmeasurelem  42772  psmeasure  42773  ssnn0ssfz  44417