Theorem elpwid 4565

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3898  𝒫 cpw 4556

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3915  df-pw 4558

This theorem is used by:  cofon1  8659  cofon2  8660  fopwdom  9082  ssenen  9148  fival  9382  dffi2  9393  elfiun  9400  tskwe  10003  acndom2  10105  fodomfi2  10111  infpwfien  10113  dfac12lem2  10195  ackbij1lem9  10277  ackbij1lem10  10278  ackbij1lem11  10279  ackbij1lem16  10284  ackbij2lem3  10290  cfss  10315  fin23lem7  10366  fin23lem11  10367  enfin2i  10371  isf32lem8  10410  isf34lem4  10427  isf34lem7  10429  isf34lem6  10430  isfin1-3  10436  fin1a2lem13  10462  ttukeylem6  10564  uzssz  12956  elfzoelz  13762  ackbijnn  15965  incexclem  15973  smuval2  16620  smupvallem  16621  smueqlem  16628  ramub1lem1  17166  ramub1lem2  17167  restid2  17563  mress  17725  mrcuni  17757  mreexexlem4d  17783  mreexexd  17784  mreexdomd  17785  isacs2  17789  acsfn  17795  isdrs2  18442  ipodrsima  18677  isacs3lem  18678  acsfiindd  18689  lagsubg2  19371  ghmqusnsg  19458  ghmquskerlem3  19462  ghmqusker  19463  cntzrcl  19503  sylow1lem2  19775  sylow1lem3  19776  sylow1lem4  19777  sylow2alem2  19794  sylow2a  19795  lsmpropd  19853  lssacs  21204  lssacsex  21384  lbsextlem2  21399  lbsextlem3  21400  lbsextlem4  21401  rhmqusnsg  21543  elocv  21936  ppttop  23287  epttop  23289  clsval2  23330  mretopd  23372  neiss2  23381  neiptopnei  23412  ordtbas  23472  subbascn  23534  discmp  23678  uncmp  23683  conncompconn  23712  1stcfb  23725  2ndcdisj  23737  restnlly  23763  nllyrest  23767  nllyidm  23770  cldllycmp  23776  1stckgenlem  23834  dfac14  23899  xkoccn  23900  txnlly  23918  txkgen  23933  xkopt  23936  xkoco2cn  23939  xkoinjcn  23968  tgqtop  23993  nrmhmph  24075  fbelss  24114  fbssfi  24118  infil  24144  alexsubALTlem3  24330  alexsubALTlem4  24331  ustssxp  24486  trust  24510  utopsnneiplem  24528  blssm  24699  blin2  24710  metustss  24832  metust  24839  psmetutop  24848  restmetu  24851  icccmplem2  25105  cncfrss  25174  cncfrss2  25175  bndth  25241  lebnum  25247  ovolicc2  25805  vitalilem5  25895  i1fd  25964  dvbsss  26184  perfdvf  26185  plybss  26474  wilthlem2  27360  oldf  28157  newf  28158  leftf  28175  rightf  28176  elmade  28177  sltsleft  28180  sltsright  28181  cofslts  28238  coinitslts  28239  f1otrg  29382  uhgrss  29576  upgrss  29600  usgrss  29689  eupth2lems  30773  ubthlem1  31406  elpwdifcl  33056  elpwiuncl  33057  ssnnssfz  33313  indf1ofs  33367  pwrssmgc  33495  trsp2cyc  33618  lmhmqusker  33902  rhmquskerlem  33909  esplylem  34132  esplymhp  34134  esplyfv1  34135  esplyfv  34136  esplyfval3  34138  exsslsb  34163  zarcmplem  34447  esumval  34612  esumel  34613  gsumesum  34625  esumlub  34626  esumpcvgval  34644  esumcvg  34652  elsigass  34691  ispisys2  34720  sigapildsyslem  34728  sigapildsys  34729  ldgenpisyslem1  34730  ldgenpisys  34733  dynkin  34734  rossspw  34736  srossspw  34743  ddemeas  34803  br2base  34836  sxbrsigalem0  34838  dya2iocucvr  34851  sxbrsigalem2  34853  sxbrsiga  34857  oms0  34864  omssubadd  34867  carsguni  34875  elcarsgss  34876  carsggect  34885  omsmeas  34890  eulerpartlemgvv  34943  coinfliplem  35046  ballotlemfmpn  35062  cvmliftmolem2  35968  cvmlift3lem8  36012  neibastop1  37069  neibastop2lem  37070  neibastop2  37071  filnetlem4  37091  cnambfre  38506  heiborlem3  38667  heiborlem5  38669  heiborlem6  38670  heiborlem10  38674  heibor  38675  mapd1o  42625  sticksstones3  43118  prjcrv0  43583  elrfi  43643  elrfirn  43644  elrfirn2  43645  ismrcd1  43647  istopclsd  43649  mrefg3  43657  aomclem2  44000  lsmfgcl  44019  lmhmfgima  44029  elmnc  44081  fpwfvss  44356  rfovcnvf1od  44948  rfovcnvfvd  44951  fsovrfovd  44953  fsovcnvlem  44957  dssmapnvod  44964  ntrk0kbimka  44983  clsk3nimkb  44984  neik0pk1imk0  44991  ntrclsfveq1  45004  ntrclsfveq2  45005  ntrclsfveq  45006  ntrclsss  45007  ntrclsiso  45011  ntrclsk2  45012  ntrclskb  45013  ntrclsk3  45014  ntrclsk13  45015  ntrclsk4  45016  ntrneifv3  45026  ntrneineine0lem  45027  ntrneineine1lem  45028  ntrneifv4  45029  ntrneiel2  45030  ntrneicls00  45033  ntrneicls11  45034  ntrneiiso  45035  ntrneik2  45036  ntrneikb  45038  ntrneixb  45039  ntrneik3  45040  ntrneix3  45041  ntrneik13  45042  ntrneix13  45043  ntrneik4w  45044  clsneiel2  45053  clsneifv3  45054  clsneifv4  45055  neicvgel2  45064  neicvgfv  45065  gneispb  45075  elpwinss  45987  stoweidlem39  46971  stoweidlem50  46982  sge0resrnlem  47335  sge0iunmptlemre  47347  psmeasurelem  47402  psmeasure  47403  tmachlem-agreeprod  47869  tmachlem-exagreecover  47878  isubgrvtxuhgr  48884  isuspgrim0  48914  isuspgrimlem  48915  uhgrimisgrgriclem  48950  ssnn0ssfz  49383  iscnrm3rlem3  49972  iscnrm3rlem8  49977  iscnrm3llem1  49979  iscnrm3llem2  49980  iscnrm3l  49981  pgindlem  50730