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  39340  elrfirn  39341  elrfirn2  39342  ismrcd1  39344  istopclsd  39346  mrefg3  39354  aomclem2  39704  lsmfgcl  39723  lmhmfgima  39733  elmnc  39785  rfovcnvf1od  40399  rfovcnvfvd  40402  fsovrfovd  40404  fsovcnvlem  40408  dssmapnvod  40415  ntrk0kbimka  40438  clsk3nimkb  40439  neik0pk1imk0  40446  ntrclsfveq1  40459  ntrclsfveq2  40460  ntrclsfveq  40461  ntrclsss  40462  ntrclsiso  40466  ntrclsk2  40467  ntrclskb  40468  ntrclsk3  40469  ntrclsk13  40470  ntrclsk4  40471  ntrneifv3  40481  ntrneineine0lem  40482  ntrneineine1lem  40483  ntrneifv4  40484  ntrneiel2  40485  ntrneicls00  40488  ntrneicls11  40489  ntrneiiso  40490  ntrneik2  40491  ntrneikb  40493  ntrneixb  40494  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  ntrneik4w  40499  clsneiel2  40508  clsneifv3  40509  clsneifv4  40510  neicvgel2  40519  neicvgfv  40520  gneispb  40530  elpwinss  41360  stoweidlem39  42373  stoweidlem50  42384  sge0resrnlem  42734  sge0iunmptlemre  42746  psmeasurelem  42801  psmeasure  42802  ssnn0ssfz  44446