Theorem elpwid 4575

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  cofon1  8639  cofon2  8640  fopwdom  9054  ssenen  9121  fival  9370  dffi2  9381  elfiun  9388  tskwe  9910  acndom2  10014  fodomfi2  10020  infpwfien  10022  dfac12lem2  10105  ackbij1lem9  10187  ackbij1lem10  10188  ackbij1lem11  10189  ackbij1lem16  10194  ackbij2lem3  10200  cfss  10225  fin23lem7  10276  fin23lem11  10277  enfin2i  10281  isf32lem8  10320  isf34lem4  10337  isf34lem7  10339  isf34lem6  10340  isfin1-3  10346  fin1a2lem13  10372  ttukeylem6  10474  uzssz  12821  elfzoelz  13627  ackbijnn  15801  incexclem  15809  smuval2  16459  smupvallem  16460  smueqlem  16467  ramub1lem1  17004  ramub1lem2  17005  restid2  17400  mress  17561  mrcuni  17589  mreexexlem4d  17615  mreexexd  17616  mreexdomd  17617  isacs2  17621  acsfn  17627  isdrs2  18274  ipodrsima  18507  isacs3lem  18508  acsfiindd  18519  lagsubg2  19133  ghmqusnsg  19221  ghmquskerlem3  19225  ghmqusker  19226  cntzrcl  19266  sylow1lem2  19536  sylow1lem3  19537  sylow1lem4  19538  sylow2alem2  19555  sylow2a  19556  lsmpropd  19614  lssacs  20880  lssacsex  21061  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  rhmqusnsg  21202  elocv  21584  ppttop  22901  epttop  22903  clsval2  22944  mretopd  22986  neiss2  22995  neiptopnei  23026  ordtbas  23086  subbascn  23148  discmp  23292  uncmp  23297  conncompconn  23326  1stcfb  23339  2ndcdisj  23350  restnlly  23376  nllyrest  23380  nllyidm  23383  cldllycmp  23389  1stckgenlem  23447  dfac14  23512  xkoccn  23513  txnlly  23531  txkgen  23546  xkopt  23549  xkoco2cn  23552  xkoinjcn  23581  tgqtop  23606  nrmhmph  23688  fbelss  23727  fbssfi  23731  infil  23757  alexsubALTlem3  23943  alexsubALTlem4  23944  ustssxp  24099  trust  24124  utopsnneiplem  24142  blssm  24313  blin2  24324  metustss  24446  metust  24453  psmetutop  24462  restmetu  24465  icccmplem2  24719  cncfrss  24791  cncfrss2  24792  bndth  24864  lebnum  24870  ovolicc2  25430  vitalilem5  25520  i1fd  25589  dvbsss  25810  perfdvf  25811  plybss  26106  wilthlem2  26986  oldf  27772  newf  27773  leftf  27784  rightf  27785  elmade  27786  ssltleft  27789  ssltright  27790  cofsslt  27833  coinitsslt  27834  f1otrg  28805  uhgrss  28998  upgrss  29022  usgrss  29108  eupth2lems  30174  ubthlem1  30806  elpwdifcl  32462  elpwiuncl  32463  ssnnssfz  32717  indf1ofs  32796  pwrssmgc  32933  trsp2cyc  33087  lmhmqusker  33395  rhmquskerlem  33403  exsslsb  33599  zarcmplem  33878  esumval  34043  esumel  34044  gsumesum  34056  esumlub  34057  esumpcvgval  34075  esumcvg  34083  elsigass  34122  ispisys2  34150  sigapildsyslem  34158  sigapildsys  34159  ldgenpisyslem1  34160  ldgenpisys  34163  dynkin  34164  rossspw  34166  srossspw  34173  ddemeas  34233  br2base  34267  sxbrsigalem0  34269  dya2iocucvr  34282  sxbrsigalem2  34284  sxbrsiga  34288  oms0  34295  omssubadd  34298  carsguni  34306  elcarsgss  34307  carsggect  34316  omsmeas  34321  eulerpartlemgvv  34374  coinfliplem  34477  ballotlemfmpn  34493  cvmliftmolem2  35276  cvmlift3lem8  35320  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  filnetlem4  36376  cnambfre  37669  heiborlem3  37814  heiborlem5  37816  heiborlem6  37817  heiborlem10  37821  heibor  37822  mapd1o  41649  sticksstones3  42143  prjcrv0  42628  elrfi  42689  elrfirn  42690  elrfirn2  42691  ismrcd1  42693  istopclsd  42695  mrefg3  42703  aomclem2  43051  lsmfgcl  43070  lmhmfgima  43080  elmnc  43132  fpwfvss  43408  rfovcnvf1od  44000  rfovcnvfvd  44003  fsovrfovd  44005  fsovcnvlem  44009  dssmapnvod  44016  ntrk0kbimka  44035  clsk3nimkb  44036  neik0pk1imk0  44043  ntrclsfveq1  44056  ntrclsfveq2  44057  ntrclsfveq  44058  ntrclsss  44059  ntrclsiso  44063  ntrclsk2  44064  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrclsk4  44068  ntrneifv3  44078  ntrneineine0lem  44079  ntrneineine1lem  44080  ntrneifv4  44081  ntrneiel2  44082  ntrneicls00  44085  ntrneicls11  44086  ntrneiiso  44087  ntrneik2  44088  ntrneikb  44090  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  ntrneik4w  44096  clsneiel2  44105  clsneifv3  44106  clsneifv4  44107  neicvgel2  44116  neicvgfv  44117  gneispb  44127  elpwinss  45050  stoweidlem39  46044  stoweidlem50  46055  sge0resrnlem  46408  sge0iunmptlemre  46420  psmeasurelem  46475  psmeasure  46476  isubgrvtxuhgr  47868  isuspgrim0  47898  isuspgrimlem  47899  uhgrimisgrgriclem  47934  ssnn0ssfz  48341  iscnrm3rlem3  48934  iscnrm3rlem8  48939  iscnrm3llem1  48941  iscnrm3llem2  48942  iscnrm3l  48943  pgindlem  49708