Theorem elpwid 4557

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3900  𝒫 cpw 4548

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3917  df-pw 4550

This theorem is referenced by:  cofon1  8582  cofon2  8583  fopwdom  8993  ssenen  9059  fival  9291  dffi2  9302  elfiun  9309  tskwe  9835  acndom2  9937  fodomfi2  9943  infpwfien  9945  dfac12lem2  10028  ackbij1lem9  10110  ackbij1lem10  10111  ackbij1lem11  10112  ackbij1lem16  10117  ackbij2lem3  10123  cfss  10148  fin23lem7  10199  fin23lem11  10200  enfin2i  10204  isf32lem8  10243  isf34lem4  10260  isf34lem7  10262  isf34lem6  10263  isfin1-3  10269  fin1a2lem13  10295  ttukeylem6  10397  uzssz  12745  elfzoelz  13551  ackbijnn  15727  incexclem  15735  smuval2  16385  smupvallem  16386  smueqlem  16393  ramub1lem1  16930  ramub1lem2  16931  restid2  17326  mress  17487  mrcuni  17519  mreexexlem4d  17545  mreexexd  17546  mreexdomd  17547  isacs2  17551  acsfn  17557  isdrs2  18204  ipodrsima  18439  isacs3lem  18440  acsfiindd  18451  lagsubg2  19099  ghmqusnsg  19187  ghmquskerlem3  19191  ghmqusker  19192  cntzrcl  19232  sylow1lem2  19504  sylow1lem3  19505  sylow1lem4  19506  sylow2alem2  19523  sylow2a  19524  lsmpropd  19582  lssacs  20893  lssacsex  21074  lbsextlem2  21089  lbsextlem3  21090  lbsextlem4  21091  rhmqusnsg  21215  elocv  21598  ppttop  22915  epttop  22917  clsval2  22958  mretopd  23000  neiss2  23009  neiptopnei  23040  ordtbas  23100  subbascn  23162  discmp  23306  uncmp  23311  conncompconn  23340  1stcfb  23353  2ndcdisj  23364  restnlly  23390  nllyrest  23394  nllyidm  23397  cldllycmp  23403  1stckgenlem  23461  dfac14  23526  xkoccn  23527  txnlly  23545  txkgen  23560  xkopt  23563  xkoco2cn  23566  xkoinjcn  23595  tgqtop  23620  nrmhmph  23702  fbelss  23741  fbssfi  23745  infil  23771  alexsubALTlem3  23957  alexsubALTlem4  23958  ustssxp  24113  trust  24137  utopsnneiplem  24155  blssm  24326  blin2  24337  metustss  24459  metust  24466  psmetutop  24475  restmetu  24478  icccmplem2  24732  cncfrss  24804  cncfrss2  24805  bndth  24877  lebnum  24883  ovolicc2  25443  vitalilem5  25533  i1fd  25602  dvbsss  25823  perfdvf  25824  plybss  26119  wilthlem2  26999  oldf  27791  newf  27792  leftf  27803  rightf  27804  elmade  27805  ssltleft  27808  ssltright  27809  cofsslt  27855  coinitsslt  27856  f1otrg  28842  uhgrss  29035  upgrss  29059  usgrss  29145  eupth2lems  30208  ubthlem1  30840  elpwdifcl  32496  elpwiuncl  32497  ssnnssfz  32760  indf1ofs  32837  pwrssmgc  32971  trsp2cyc  33082  lmhmqusker  33372  rhmquskerlem  33380  esplylem  33577  esplymhp  33579  esplyfv1  33580  esplyfv  33581  exsslsb  33599  zarcmplem  33884  esumval  34049  esumel  34050  gsumesum  34062  esumlub  34063  esumpcvgval  34081  esumcvg  34089  elsigass  34128  ispisys2  34156  sigapildsyslem  34164  sigapildsys  34165  ldgenpisyslem1  34166  ldgenpisys  34169  dynkin  34170  rossspw  34172  srossspw  34179  ddemeas  34239  br2base  34272  sxbrsigalem0  34274  dya2iocucvr  34287  sxbrsigalem2  34289  sxbrsiga  34293  oms0  34300  omssubadd  34303  carsguni  34311  elcarsgss  34312  carsggect  34321  omsmeas  34326  eulerpartlemgvv  34379  coinfliplem  34482  ballotlemfmpn  34498  cvmliftmolem2  35294  cvmlift3lem8  35338  neibastop1  36372  neibastop2lem  36373  neibastop2  36374  filnetlem4  36394  cnambfre  37687  heiborlem3  37832  heiborlem5  37834  heiborlem6  37835  heiborlem10  37839  heibor  37840  mapd1o  41666  sticksstones3  42160  prjcrv0  42645  elrfi  42706  elrfirn  42707  elrfirn2  42708  ismrcd1  42710  istopclsd  42712  mrefg3  42720  aomclem2  43067  lsmfgcl  43086  lmhmfgima  43096  elmnc  43148  fpwfvss  43424  rfovcnvf1od  44016  rfovcnvfvd  44019  fsovrfovd  44021  fsovcnvlem  44025  dssmapnvod  44032  ntrk0kbimka  44051  clsk3nimkb  44052  neik0pk1imk0  44059  ntrclsfveq1  44072  ntrclsfveq2  44073  ntrclsfveq  44074  ntrclsss  44075  ntrclsiso  44079  ntrclsk2  44080  ntrclskb  44081  ntrclsk3  44082  ntrclsk13  44083  ntrclsk4  44084  ntrneifv3  44094  ntrneineine0lem  44095  ntrneineine1lem  44096  ntrneifv4  44097  ntrneiel2  44098  ntrneicls00  44101  ntrneicls11  44102  ntrneiiso  44103  ntrneik2  44104  ntrneikb  44106  ntrneixb  44107  ntrneik3  44108  ntrneix3  44109  ntrneik13  44110  ntrneix13  44111  ntrneik4w  44112  clsneiel2  44121  clsneifv3  44122  clsneifv4  44123  neicvgel2  44132  neicvgfv  44133  gneispb  44143  elpwinss  45065  stoweidlem39  46056  stoweidlem50  46067  sge0resrnlem  46420  sge0iunmptlemre  46432  psmeasurelem  46487  psmeasure  46488  isubgrvtxuhgr  47874  isuspgrim0  47904  isuspgrimlem  47905  uhgrimisgrgriclem  47940  ssnn0ssfz  48359  iscnrm3rlem3  48952  iscnrm3rlem8  48957  iscnrm3llem1  48959  iscnrm3llem2  48960  iscnrm3l  48961  pgindlem  49726