Theorem elpwid 4612

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  cofon1  8671  cofon2  8672  fopwdom  9080  ssenen  9151  fival  9407  dffi2  9418  elfiun  9425  tskwe  9945  acndom2  10049  fodomfi2  10055  infpwfien  10057  dfac12lem2  10139  ackbij1lem9  10223  ackbij1lem10  10224  ackbij1lem11  10225  ackbij1lem16  10230  ackbij2lem3  10236  cfss  10260  fin23lem7  10311  fin23lem11  10312  enfin2i  10316  isf32lem8  10355  isf34lem4  10372  isf34lem7  10374  isf34lem6  10375  isfin1-3  10381  fin1a2lem13  10407  ttukeylem6  10509  uzssz  12843  elfzoelz  13632  ackbijnn  15774  incexclem  15782  smuval2  16423  smupvallem  16424  smueqlem  16431  ramub1lem1  16959  ramub1lem2  16960  restid2  17376  mress  17537  mrcuni  17565  mreexexlem4d  17591  mreexexd  17592  mreexdomd  17593  isacs2  17597  acsfn  17603  isdrs2  18259  ipodrsima  18494  isacs3lem  18495  acsfiindd  18506  lagsubg2  19071  cntzrcl  19191  sylow1lem2  19467  sylow1lem3  19468  sylow1lem4  19469  sylow2alem2  19486  sylow2a  19487  lsmpropd  19545  lssacs  20578  lssacsex  20757  lbsextlem2  20772  lbsextlem3  20773  lbsextlem4  20774  elocv  21221  ppttop  22510  epttop  22512  clsval2  22554  mretopd  22596  neiss2  22605  neiptopnei  22636  ordtbas  22696  subbascn  22758  discmp  22902  uncmp  22907  conncompconn  22936  1stcfb  22949  2ndcdisj  22960  restnlly  22986  nllyrest  22990  nllyidm  22993  cldllycmp  22999  1stckgenlem  23057  dfac14  23122  xkoccn  23123  txnlly  23141  txkgen  23156  xkopt  23159  xkoco2cn  23162  xkoinjcn  23191  tgqtop  23216  nrmhmph  23298  fbelss  23337  fbssfi  23341  infil  23367  alexsubALTlem3  23553  alexsubALTlem4  23554  ustssxp  23709  trust  23734  utopsnneiplem  23752  blssm  23924  blin2  23935  metustss  24060  metust  24067  psmetutop  24076  restmetu  24079  icccmplem2  24339  cncfrss  24407  cncfrss2  24408  bndth  24474  lebnum  24480  ovolicc2  25039  vitalilem5  25129  i1fd  25198  dvbsss  25419  perfdvf  25420  plybss  25708  wilthlem2  26573  oldf  27353  newf  27354  leftf  27361  rightf  27362  elmade  27363  ssltleft  27366  ssltright  27367  cofsslt  27407  coinitsslt  27408  f1otrg  28153  uhgrss  28355  upgrss  28379  usgrss  28465  eupth2lems  29522  ubthlem1  30154  elpwdifcl  31795  elpwiuncl  31796  ssnnssfz  32029  pwrssmgc  32201  trsp2cyc  32313  ghmquskerlem3  32562  ghmqusker  32563  lmhmqusker  32565  rhmquskerlem  32574  zarcmplem  32892  indf1ofs  33055  esumval  33075  esumel  33076  gsumesum  33088  esumlub  33089  esumpcvgval  33107  esumcvg  33115  elsigass  33154  ispisys2  33182  sigapildsyslem  33190  sigapildsys  33191  ldgenpisyslem1  33192  ldgenpisys  33195  dynkin  33196  rossspw  33198  srossspw  33205  ddemeas  33265  br2base  33299  sxbrsigalem0  33301  dya2iocucvr  33314  sxbrsigalem2  33316  sxbrsiga  33320  oms0  33327  omssubadd  33330  carsguni  33338  elcarsgss  33339  carsggect  33348  omsmeas  33353  eulerpartlemgvv  33406  coinfliplem  33508  ballotlemfmpn  33524  cvmliftmolem2  34304  cvmlift3lem8  34348  neibastop1  35292  neibastop2lem  35293  neibastop2  35294  filnetlem4  35314  cnambfre  36584  heiborlem3  36729  heiborlem5  36731  heiborlem6  36732  heiborlem10  36736  heibor  36737  mapd1o  40567  sticksstones3  41012  prjcrv0  41423  elrfi  41480  elrfirn  41481  elrfirn2  41482  ismrcd1  41484  istopclsd  41486  mrefg3  41494  aomclem2  41845  lsmfgcl  41864  lmhmfgima  41874  elmnc  41926  fpwfvss  42211  rfovcnvf1od  42803  rfovcnvfvd  42806  fsovrfovd  42808  fsovcnvlem  42812  dssmapnvod  42819  ntrk0kbimka  42838  clsk3nimkb  42839  neik0pk1imk0  42846  ntrclsfveq1  42859  ntrclsfveq2  42860  ntrclsfveq  42861  ntrclsss  42862  ntrclsiso  42866  ntrclsk2  42867  ntrclskb  42868  ntrclsk3  42869  ntrclsk13  42870  ntrclsk4  42871  ntrneifv3  42881  ntrneineine0lem  42882  ntrneineine1lem  42883  ntrneifv4  42884  ntrneiel2  42885  ntrneicls00  42888  ntrneicls11  42889  ntrneiiso  42890  ntrneik2  42891  ntrneikb  42893  ntrneixb  42894  ntrneik3  42895  ntrneix3  42896  ntrneik13  42897  ntrneix13  42898  ntrneik4w  42899  clsneiel2  42908  clsneifv3  42909  clsneifv4  42910  neicvgel2  42919  neicvgfv  42920  gneispb  42930  elpwinss  43784  stoweidlem39  44803  stoweidlem50  44814  sge0resrnlem  45167  sge0iunmptlemre  45179  psmeasurelem  45234  psmeasure  45235  ssnn0ssfz  47073  iscnrm3rlem3  47623  iscnrm3rlem8  47628  iscnrm3llem1  47630  iscnrm3llem2  47631  iscnrm3l  47632  pgindlem  47808