Theorem elpwid 4551

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  cofon1  8599  cofon2  8600  fopwdom  9014  ssenen  9080  fival  9316  dffi2  9327  elfiun  9334  tskwe  9863  acndom2  9965  fodomfi2  9971  infpwfien  9973  dfac12lem2  10056  ackbij1lem9  10138  ackbij1lem10  10139  ackbij1lem11  10140  ackbij1lem16  10145  ackbij2lem3  10151  cfss  10176  fin23lem7  10227  fin23lem11  10228  enfin2i  10232  isf32lem8  10271  isf34lem4  10288  isf34lem7  10290  isf34lem6  10291  isfin1-3  10297  fin1a2lem13  10323  ttukeylem6  10425  uzssz  12798  elfzoelz  13602  ackbijnn  15782  incexclem  15790  smuval2  16440  smupvallem  16441  smueqlem  16448  ramub1lem1  16986  ramub1lem2  16987  restid2  17382  mress  17544  mrcuni  17576  mreexexlem4d  17602  mreexexd  17603  mreexdomd  17604  isacs2  17608  acsfn  17614  isdrs2  18261  ipodrsima  18496  isacs3lem  18497  acsfiindd  18508  lagsubg2  19158  ghmqusnsg  19246  ghmquskerlem3  19250  ghmqusker  19251  cntzrcl  19291  sylow1lem2  19563  sylow1lem3  19564  sylow1lem4  19565  sylow2alem2  19582  sylow2a  19583  lsmpropd  19641  lssacs  20951  lssacsex  21132  lbsextlem2  21147  lbsextlem3  21148  lbsextlem4  21149  rhmqusnsg  21273  elocv  21656  ppttop  22981  epttop  22983  clsval2  23024  mretopd  23066  neiss2  23075  neiptopnei  23106  ordtbas  23166  subbascn  23228  discmp  23372  uncmp  23377  conncompconn  23406  1stcfb  23419  2ndcdisj  23430  restnlly  23456  nllyrest  23460  nllyidm  23463  cldllycmp  23469  1stckgenlem  23527  dfac14  23592  xkoccn  23593  txnlly  23611  txkgen  23626  xkopt  23629  xkoco2cn  23632  xkoinjcn  23661  tgqtop  23686  nrmhmph  23768  fbelss  23807  fbssfi  23811  infil  23837  alexsubALTlem3  24023  alexsubALTlem4  24024  ustssxp  24179  trust  24203  utopsnneiplem  24221  blssm  24392  blin2  24403  metustss  24525  metust  24532  psmetutop  24541  restmetu  24544  icccmplem2  24798  cncfrss  24867  cncfrss2  24868  bndth  24934  lebnum  24940  ovolicc2  25498  vitalilem5  25588  i1fd  25657  dvbsss  25878  perfdvf  25879  plybss  26171  wilthlem2  27050  oldf  27848  newf  27849  leftf  27866  rightf  27867  elmade  27868  sltsleft  27871  sltsright  27872  cofslts  27929  coinitslts  27930  f1otrg  28958  uhgrss  29152  upgrss  29176  usgrss  29262  eupth2lems  30328  ubthlem1  30961  elpwdifcl  32616  elpwiuncl  32617  ssnnssfz  32880  indf1ofs  32946  pwrssmgc  33080  trsp2cyc  33204  lmhmqusker  33497  rhmquskerlem  33505  esplylem  33730  esplymhp  33732  esplyfv1  33733  esplyfv  33734  esplyfval3  33736  exsslsb  33761  zarcmplem  34046  esumval  34211  esumel  34212  gsumesum  34224  esumlub  34225  esumpcvgval  34243  esumcvg  34251  elsigass  34290  ispisys2  34318  sigapildsyslem  34326  sigapildsys  34327  ldgenpisyslem1  34328  ldgenpisys  34331  dynkin  34332  rossspw  34334  srossspw  34341  ddemeas  34401  br2base  34434  sxbrsigalem0  34436  dya2iocucvr  34449  sxbrsigalem2  34451  sxbrsiga  34455  oms0  34462  omssubadd  34465  carsguni  34473  elcarsgss  34474  carsggect  34483  omsmeas  34488  eulerpartlemgvv  34541  coinfliplem  34644  ballotlemfmpn  34660  cvmliftmolem2  35485  cvmlift3lem8  35529  neibastop1  36562  neibastop2lem  36563  neibastop2  36564  filnetlem4  36584  cnambfre  38000  heiborlem3  38145  heiborlem5  38147  heiborlem6  38148  heiborlem10  38152  heibor  38153  mapd1o  42105  sticksstones3  42598  prjcrv0  43077  elrfi  43137  elrfirn  43138  elrfirn2  43139  ismrcd1  43141  istopclsd  43143  mrefg3  43151  aomclem2  43498  lsmfgcl  43517  lmhmfgima  43527  elmnc  43579  fpwfvss  43854  rfovcnvf1od  44446  rfovcnvfvd  44449  fsovrfovd  44451  fsovcnvlem  44455  dssmapnvod  44462  ntrk0kbimka  44481  clsk3nimkb  44482  neik0pk1imk0  44489  ntrclsfveq1  44502  ntrclsfveq2  44503  ntrclsfveq  44504  ntrclsss  44505  ntrclsiso  44509  ntrclsk2  44510  ntrclskb  44511  ntrclsk3  44512  ntrclsk13  44513  ntrclsk4  44514  ntrneifv3  44524  ntrneineine0lem  44525  ntrneineine1lem  44526  ntrneifv4  44527  ntrneiel2  44528  ntrneicls00  44531  ntrneicls11  44532  ntrneiiso  44533  ntrneik2  44534  ntrneikb  44536  ntrneixb  44537  ntrneik3  44538  ntrneix3  44539  ntrneik13  44540  ntrneix13  44541  ntrneik4w  44542  clsneiel2  44551  clsneifv3  44552  clsneifv4  44553  neicvgel2  44562  neicvgfv  44563  gneispb  44573  elpwinss  45495  stoweidlem39  46482  stoweidlem50  46493  sge0resrnlem  46846  sge0iunmptlemre  46858  psmeasurelem  46913  psmeasure  46914  isubgrvtxuhgr  48337  isuspgrim0  48367  isuspgrimlem  48368  uhgrimisgrgriclem  48403  ssnn0ssfz  48822  iscnrm3rlem3  49414  iscnrm3rlem8  49419  iscnrm3llem1  49421  iscnrm3llem2  49422  iscnrm3l  49423  pgindlem  50187