Theorem elpwid 4170

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

Syntax hints:   → wi 4   ∈ wcel 1990   ⊆ wss 3574  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  fopwdom  8068  ssenen  8134  fival  8318  dffi2  8329  elfiun  8336  tskwe  8776  acndom2  8877  fodomfi2  8883  infpwfien  8885  dfac12lem2  8966  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1lem11  9052  ackbij1lem16  9057  ackbij2lem3  9063  cfss  9087  fin23lem7  9138  fin23lem11  9139  enfin2i  9143  isf32lem8  9182  isf34lem4  9199  isf34lem7  9201  isf34lem6  9202  isfin1-3  9208  fin1a2lem13  9234  ttukeylem6  9336  uzssz  11707  elfzoelz  12470  ackbijnn  14560  incexclem  14568  smuval2  15204  smupvallem  15205  smueqlem  15212  ramub1lem1  15730  ramub1lem2  15731  restid2  16091  mress  16253  mrcuni  16281  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309  mreexdomd  16310  acsfn  16320  isdrs2  16939  ipodrsima  17165  isacs3lem  17166  acsfiindd  17177  lagsubg2  17655  cntzrcl  17760  sylow1lem2  18014  sylow1lem3  18015  sylow1lem4  18016  sylow2alem2  18033  sylow2a  18034  lsmpropd  18090  lssacs  18967  lssacsex  19144  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  elocv  20012  ppttop  20811  epttop  20813  clsval2  20854  mretopd  20896  neiss2  20905  neiptopnei  20936  ordtbas  20996  subbascn  21058  discmp  21201  uncmp  21206  conncompconn  21235  1stcfb  21248  2ndcdisj  21259  restnlly  21285  nllyrest  21289  nllyidm  21292  cldllycmp  21298  1stckgenlem  21356  dfac14  21421  xkoccn  21422  txnlly  21440  txkgen  21455  xkopt  21458  xkoco2cn  21461  xkoinjcn  21490  tgqtop  21515  nrmhmph  21597  fbelss  21637  fbssfi  21641  infil  21667  alexsubALTlem3  21853  alexsubALTlem4  21854  ustssxp  22008  trust  22033  utopsnneiplem  22051  blssm  22223  blin2  22234  metustss  22356  metustfbas  22362  metust  22363  psmetutop  22372  restmetu  22375  icccmplem2  22626  cncfrss  22694  cncfrss2  22695  bndth  22757  lebnum  22763  ovolicc2  23290  vitalilem5  23381  i1fd  23448  dvbsss  23666  perfdvf  23667  plybss  23950  wilthlem2  24795  f1otrg  25751  uhgrss  25959  upgrss  25983  usgrss  26069  eupth2lems  27098  ubthlem1  27726  elpwdifcl  29358  elpwiuncl  29359  ssnnssfz  29549  indf1ofs  30088  esumval  30108  esumel  30109  gsumesum  30121  esumlub  30122  esumpcvgval  30140  esumcvg  30148  elsigass  30188  ispisys2  30216  sigapildsyslem  30224  sigapildsys  30225  ldgenpisyslem1  30226  ldgenpisys  30229  dynkin  30230  rossspw  30232  srossspw  30239  ddemeas  30299  br2base  30331  sxbrsigalem0  30333  dya2iocucvr  30346  sxbrsigalem2  30348  sxbrsiga  30352  oms0  30359  omssubadd  30362  carsguni  30370  elcarsgss  30371  carsggect  30380  omsmeas  30385  eulerpartlemgvv  30438  coinfliplem  30540  ballotlemfmpn  30556  cvmliftmolem2  31264  cvmlift3lem8  31308  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  filnetlem4  32376  cnambfre  33458  heiborlem3  33612  heiborlem5  33614  heiborlem6  33615  heiborlem10  33619  heibor  33620  mapd1o  36937  elrfi  37257  elrfirn  37258  elrfirn2  37259  ismrcd1  37261  istopclsd  37263  mrefg3  37271  aomclem2  37625  lsmfgcl  37644  lmhmfgima  37654  elmnc  37706  rfovcnvf1od  38298  rfovcnvfvd  38301  fsovrfovd  38303  fsovcnvlem  38307  dssmapnvod  38314  ntrk0kbimka  38337  clsk3nimkb  38338  neik0pk1imk0  38345  ntrclsfveq1  38358  ntrclsfveq2  38359  ntrclsfveq  38360  ntrclsss  38361  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  ntrneifv3  38380  ntrneineine0lem  38381  ntrneineine1lem  38382  ntrneifv4  38383  ntrneiel2  38384  ntrneicls00  38387  ntrneicls11  38388  ntrneiiso  38389  ntrneik2  38390  ntrneikb  38392  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  clsneiel2  38407  clsneifv3  38408  clsneifv4  38409  neicvgel2  38418  neicvgfv  38419  gneispb  38429  elpwinss  39216  stoweidlem39  40256  stoweidlem50  40267  sge0resrnlem  40620  sge0iunmptlemre  40632  psmeasurelem  40687  psmeasure  40688  ssnn0ssfz  42127