Theorem elpwid 4569

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-pw 4562

This theorem is used by:  cofon1  8709  cofon2  8710  fopwdom  9132  ssenen  9198  fival  9431  dffi2  9442  elfiun  9449  tskwe  10058  acndom2  10160  fodomfi2  10166  infpwfien  10168  dfac12lem2  10250  ackbij1lem9  10332  ackbij1lem10  10333  ackbij1lem11  10334  ackbij1lem16  10339  ackbij2lem3  10345  cfss  10370  fin23lem7  10421  fin23lem11  10422  enfin2i  10426  isf32lem8  10465  isf34lem4  10482  isf34lem7  10484  isf34lem6  10485  isfin1-3  10491  fin1a2lem13  10517  ttukeylem6  10619  uzssz  13013  elfzoelz  13820  ackbijnn  16026  incexclem  16034  smuval2  16681  smupvallem  16682  smueqlem  16689  ramub1lem1  17233  ramub1lem2  17234  restid2  17630  mress  17792  mrcuni  17824  mreexexlem4d  17850  mreexexd  17851  mreexdomd  17852  isacs2  17856  acsfn  17862  isdrs2  18509  ipodrsima  18744  isacs3lem  18745  acsfiindd  18756  lagsubg2  19438  ghmqusnsg  19526  ghmquskerlem3  19530  ghmqusker  19531  cntzrcl  19571  sylow1lem2  19843  sylow1lem3  19844  sylow1lem4  19845  sylow2alem2  19862  sylow2a  19863  lsmpropd  19921  lssacs  21272  lssacsex  21452  lbsextlem2  21467  lbsextlem3  21468  lbsextlem4  21469  rhmqusnsg  21611  elocv  22004  ppttop  23355  epttop  23357  clsval2  23398  mretopd  23440  neiss2  23449  neiptopnei  23480  ordtbas  23540  subbascn  23602  discmp  23746  uncmp  23751  conncompconn  23780  1stcfb  23793  2ndcdisj  23805  restnlly  23831  nllyrest  23835  nllyidm  23838  cldllycmp  23844  1stckgenlem  23902  dfac14  23967  xkoccn  23968  txnlly  23986  txkgen  24001  xkopt  24004  xkoco2cn  24007  xkoinjcn  24036  tgqtop  24061  nrmhmph  24143  fbelss  24182  fbssfi  24186  infil  24212  alexsubALTlem3  24398  alexsubALTlem4  24399  ustssxp  24554  trust  24578  utopsnneiplem  24596  blssm  24767  blin2  24778  metustss  24900  metust  24907  psmetutop  24916  restmetu  24919  icccmplem2  25173  cncfrss  25242  cncfrss2  25243  bndth  25309  lebnum  25315  ovolicc2  25873  vitalilem5  25963  i1fd  26032  dvbsss  26252  perfdvf  26253  plybss  26542  wilthlem2  27426  oldf  28253  newf  28254  leftf  28271  rightf  28272  elmade  28273  sltsleft  28276  sltsright  28277  cofslts  28334  coinitslts  28335  f1otrg  29478  uhgrss  29672  upgrss  29696  usgrss  29785  eupth2lems  30869  ubthlem1  31502  elpwdifcl  33194  elpwiuncl  33195  ssnnssfz  33449  indf1ofs  33503  pwrssmgc  33631  trsp2cyc  33754  lmhmqusker  34038  rhmquskerlem  34045  esplylem  34268  esplymhp  34270  esplyfv1  34271  esplyfv  34272  esplyfval3  34274  exsslsb  34299  cmpcref  34552  zarcmplem  34583  esumval  34748  esumel  34749  gsumesum  34761  esumlub  34762  esumpcvgval  34780  esumcvg  34788  elsigass  34827  ispisys2  34856  sigapildsyslem  34864  sigapildsys  34865  ldgenpisyslem1  34866  ldgenpisys  34869  dynkin  34870  rossspw  34872  srossspw  34879  ddemeas  34939  br2base  34971  sxbrsigalem0  34973  dya2iocucvr  34986  sxbrsigalem2  34988  sxbrsiga  34992  oms0  34999  omssubadd  35002  carsguni  35010  elcarsgss  35011  carsggect  35020  omsmeas  35025  eulerpartlemgvv  35078  coinfliplem  35181  ballotlemfmpn  35197  cvmliftmolem2  36214  cvmlift3lem8  36258  neibastop1  37325  neibastop2lem  37326  neibastop2  37327  filnetlem4  37347  cnambfre  38778  heiborlem3  38939  heiborlem5  38941  heiborlem6  38942  heiborlem10  38946  heibor  38947  mapd1o  42897  sticksstones3  43390  elprjspnss  43843  elrfi  43898  elrfirn  43899  elrfirn2  43900  ismrcd1  43902  istopclsd  43904  mrefg3  43912  aomclem2  44250  lsmfgcl  44269  lmhmfgima  44279  elmnc  44330  fpwfvss  44605  rfovcnvf1od  45196  rfovcnvfvd  45199  fsovrfovd  45201  fsovcnvlem  45205  dssmapnvod  45212  ntrk0kbimka  45231  clsk3nimkb  45232  neik0pk1imk0  45239  ntrclsfveq1  45252  ntrclsfveq2  45253  ntrclsfveq  45254  ntrclsss  45255  ntrclsiso  45259  ntrclsk2  45260  ntrclskb  45261  ntrclsk3  45262  ntrclsk13  45263  ntrclsk4  45264  ntrneifv3  45274  ntrneineine0lem  45275  ntrneineine1lem  45276  ntrneifv4  45277  ntrneiel2  45278  ntrneicls00  45281  ntrneicls11  45282  ntrneiiso  45283  ntrneik2  45284  ntrneikb  45286  ntrneixb  45287  ntrneik3  45288  ntrneix3  45289  ntrneik13  45290  ntrneix13  45291  ntrneik4w  45292  clsneiel2  45301  clsneifv3  45302  clsneifv4  45303  neicvgel2  45312  neicvgfv  45313  gneispb  45323  hfstructfun  46224  rnhfstructsshf  46225  elpwinss  46271  stoweidlem39  47254  stoweidlem50  47265  sge0resrnlem  47618  sge0iunmptlemre  47630  psmeasurelem  47685  psmeasure  47686  tmachlem-agreeprod  48152  tmachlem-exagreecover  48161  isubgrvtxuhgr  49167  isuspgrim0  49197  isuspgrimlem  49198  uhgrimisgrgriclem  49233  ssnn0ssfz  49666  iscnrm3rlem3  50261  iscnrm3rlem8  50266  iscnrm3llem1  50268  iscnrm3llem2  50269  iscnrm3l  50270  parhomss2  50961  parhomss  50962  pgindlem  51088