Theorem elpwi 4611

Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)

Assertion

Ref	Expression
elpwi	⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwi

Step	Hyp	Ref	Expression
1		elpwg 4607	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-pw 4606

This theorem is referenced by:  elpwid  4613  elelpwi  4614  elpwunsn  4688  elpw2g  5338  f1opw2  7687  eldifpw  7786  pwuncl  7788  iunpw  7789  mptcnfimad  8009  f1opwfi  9393  fi0  9457  marypha1lem  9470  marypha1  9471  marypha2  9476  brwdom2  9610  brwdom3  9619  r1pwss  9821  rankpwi  9860  acndom  10088  acnnum  10089  dfac12r  10184  ackbij2lem1  10255  ackbij1lem6  10261  ackbij1b  10275  isfin2-2  10356  ssfin2  10357  enfin2i  10358  compsscnvlem  10407  compssiso  10411  fin11a  10420  enfin1ai  10421  fin12  10450  fin1a2s  10451  fin1a2  10452  hsmexlem2  10464  tskwe2  10810  inttsk  10811  inatsk  10815  hashbclem  14487  pr2pwpr  14514  elss2prb  14523  qshash  15859  incexclem  15868  incexc  15869  incexc2  15870  rpnnen2lem12  16257  smupf  16511  ramval  17041  ramlb  17052  mrcflem  17650  isacs2  17697  mreacs  17702  acsfn  17703  acsfn1  17705  acsfn2  17707  sscpwex  17862  isacs3lem  18599  isacs4lem  18601  isacs5lem  18602  isacs5  18605  pmtrfrn  19490  oppglsm  19674  acsfn1p  20816  lspf  20989  pptbas  23030  clsf  23071  mretopd  23115  neiptopuni  23153  cncls2  23296  cncls  23297  cnntr  23298  restcnrm  23385  cncmp  23415  tgcmp  23424  uncmp  23426  sscmp  23428  hauscmplem  23429  cmpfi  23431  1stcrest  23476  dis2ndc  23483  lly1stc  23519  dislly  23520  comppfsc  23555  kgentopon  23561  kgen2ss  23578  kgencn  23579  kgencn2  23580  kgencn3  23581  txcmplem2  23665  txcmp  23666  tx1stc  23673  txkgen  23675  xkopt  23678  xkococnlem  23682  xkococn  23683  kqnrmlem1  23766  kqnrmlem2  23767  hmphdis  23819  isfil2  23879  isfild  23881  fbasfip  23891  neifil  23903  trfil2  23910  trufil  23933  fixufil  23945  cfinufil  23951  fin1aufil  23955  fclscmp  24053  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem5  24079  tgpconncompeqg  24135  imasf1oxms  24517  met2ndc  24551  zdis  24851  icccmp  24860  ovolf  25530  ismbl2  25575  cmmbl  25582  nulmbl  25583  nulmbl2  25584  unmbl  25585  shftmbl  25586  voliunlem2  25599  ioombl1  25610  uniioombl  25637  sqff1o  27239  musum  27248  nulsslt  27856  nulssgt  27857  madessno  27913  oldssno  27914  newssno  27915  madebdayim  27940  eengtrkg  29015  edgssv2  29229  upgrreslem  29335  umgrreslem  29336  umgrres1lem  29341  upgrres1  29344  uhgrvd00  29566  rabfodom  32532  elpwincl1  32552  fpwrelmap  32750  cmpcref  33810  pcmplfinf  33821  zarclsint  33832  zarcls  33834  esumcst  34043  esumfsup  34050  esum2d  34073  dmvlsiga  34109  pwsiga  34110  sigaclci  34112  sigainb  34116  insiga  34117  pwldsys  34137  ldgenpisyslem1  34143  ldgenpisyslem3  34145  measinb  34201  measres  34202  cntmeas  34206  volmeas  34211  ddemeas  34216  dya2iocucvr  34265  sxbrsigalem1  34266  omscl  34276  omsf  34277  omsmon  34279  baselcarsg  34287  difelcarsg  34291  carsgsiga  34303  omsmeas  34304  coinflippv  34464  kur14  35200  connpconn  35219  cvmsi  35249  neibastop1  36341  neibastop2lem  36342  neibastop3  36344  onsucsuccmpi  36425  limsucncmpi  36427  bj-elpwg  37034  bj-0int  37083  bj-ismooredr  37091  lindsdom  37600  ismblfin  37647  cover2  37701  sstotbnd3  37762  heibor1  37796  heibor  37807  pclvalN  39872  pclfinN  39882  pclcmpatN  39883  dochfN  41338  elrfi  42681  cmpfiiin  42684  ismrcd2  42686  isnacs3  42697  aomclem2  43043  islssfg  43058  lmhmfgsplit  43074  lnrfg  43107  dfno2  43417  rfovcnvf1od  43993  dssmapnvod  44009  neik0pk1imk0  44036  isotone2  44038  ntrclsneine0lem  44053  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneix2  44082  ntrneik13  44087  ntrrn  44111  dssmapntrcls  44117  ismnushort  44296  sspwtr  44818  sspwtrALT  44819  sspwtrALT2  44820  pwtrVD  44821  pwtrrVD  44822  sspwimp  44915  sspwimpVD  44916  sspwimpcf  44917  sspwimpcfVD  44918  sspwimpALT  44922  sspwimpALT2  44925  pwssfi  44984  ssnnf1octb  45136  dvdmsscn  45891  dvnmptconst  45896  dvnxpaek  45897  dvnmul  45898  dvnprodlem3  45903  ismbl3  45941  ismbl4  45948  stoweidlem57  46012  pwsal  46270  prsal  46273  intsal  46285  salexct  46289  issalnnd  46300  sge0rnre  46319  sge0tsms  46335  sge0cl  46336  sge0fsum  46342  sge0sup  46346  sge0less  46347  sge0gerp  46350  sge0resplit  46361  sge0split  46364  nnfoctbdj  46411  ismeannd  46422  psmeasure  46426  caragen0  46461  caragenunidm  46463  caragenuncl  46468  caragendifcl  46469  omeiunle  46472  carageniuncl  46478  caragensal  46480  caratheodorylem2  46482  0ome  46484  isomennd  46486  caragenel2d  46487  caragencmpl  46490  ovnf  46518  ovn02  46523  ovnsubaddlem1  46525  ovnsubaddlem2  46526  ovnsubadd  46527  hspmbl  46584  isvonmbl  46593  vonmblss2  46597  ovnsubadd2lem  46600  vonvolmbl  46616  nsssmfmbf  46734  smfresal  46743  smfpimbor1lem2  46754  sprsymrelfv  47418  prpair  47425  grtriprop  47845  lincdifsn  48269  lcosslsp  48283  lindslinindsimp1  48302  lincresunit3lem1  48324  lincresunit3lem2  48325  lincresunit3  48326  isclatd  48771  elpglem1  48941  aacllem  49031