Theorem elpwi 4614

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 4610	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 266	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3947  𝒫 cpw 4607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ss 3964  df-pw 4609

This theorem is referenced by:  elpwid  4616  elelpwi  4617  elpwunsn  4692  elpw2g  5351  f1opw2  7681  eldifpw  7776  pwuncl  7778  iunpw  7779  mptcnfimad  8000  f1opwfi  9400  fi0  9463  marypha1lem  9476  marypha1  9477  marypha2  9482  brwdom2  9616  brwdom3  9625  r1pwss  9827  rankpwi  9866  acndom  10094  acnnum  10095  dfac12r  10189  ackbij2lem1  10262  ackbij1lem6  10268  ackbij1b  10282  isfin2-2  10362  ssfin2  10363  enfin2i  10364  compsscnvlem  10413  compssiso  10417  fin11a  10426  enfin1ai  10427  fin12  10456  fin1a2s  10457  fin1a2  10458  hsmexlem2  10470  tskwe2  10816  inttsk  10817  inatsk  10821  hashbclem  14469  pr2pwpr  14498  elss2prb  14506  qshash  15831  incexclem  15840  incexc  15841  incexc2  15842  rpnnen2lem12  16227  smupf  16478  ramval  17010  ramlb  17021  mrcflem  17619  isacs2  17666  mreacs  17671  acsfn  17672  acsfn1  17674  acsfn2  17676  sscpwex  17831  isacs3lem  18567  isacs4lem  18569  isacs5lem  18570  isacs5  18573  pmtrfrn  19456  oppglsm  19640  acsfn1p  20778  lspf  20951  pptbas  23002  clsf  23043  mretopd  23087  neiptopuni  23125  cncls2  23268  cncls  23269  cnntr  23270  restcnrm  23357  cncmp  23387  tgcmp  23396  uncmp  23398  sscmp  23400  hauscmplem  23401  cmpfi  23403  1stcrest  23448  dis2ndc  23455  lly1stc  23491  dislly  23492  comppfsc  23527  kgentopon  23533  kgen2ss  23550  kgencn  23551  kgencn2  23552  kgencn3  23553  txcmplem2  23637  txcmp  23638  tx1stc  23645  txkgen  23647  xkopt  23650  xkococnlem  23654  xkococn  23655  kqnrmlem1  23738  kqnrmlem2  23739  hmphdis  23791  isfil2  23851  isfild  23853  fbasfip  23863  neifil  23875  trfil2  23882  trufil  23905  fixufil  23917  cfinufil  23923  fin1aufil  23927  fclscmp  24025  alexsubALTlem2  24043  alexsubALTlem3  24044  alexsubALTlem4  24045  ptcmplem5  24051  tgpconncompeqg  24107  imasf1oxms  24489  met2ndc  24523  zdis  24823  icccmp  24832  ovolf  25502  ismbl2  25547  cmmbl  25554  nulmbl  25555  nulmbl2  25556  unmbl  25557  shftmbl  25558  voliunlem2  25571  ioombl1  25582  uniioombl  25609  sqff1o  27210  musum  27219  nulsslt  27827  nulssgt  27828  madessno  27884  oldssno  27885  newssno  27886  madebdayim  27911  eengtrkg  28920  edgssv2  29134  upgrreslem  29240  umgrreslem  29241  umgrres1lem  29246  upgrres1  29249  uhgrvd00  29471  rabfodom  32431  elpwincl1  32452  fpwrelmap  32647  cmpcref  33665  pcmplfinf  33676  zarclsint  33687  zarcls  33689  esumcst  33896  esumfsup  33903  esum2d  33926  dmvlsiga  33962  pwsiga  33963  sigaclci  33965  sigainb  33969  insiga  33970  pwldsys  33990  ldgenpisyslem1  33996  ldgenpisyslem3  33998  measinb  34054  measres  34055  cntmeas  34059  volmeas  34064  ddemeas  34069  dya2iocucvr  34118  sxbrsigalem1  34119  omscl  34129  omsf  34130  omsmon  34132  baselcarsg  34140  difelcarsg  34144  carsgsiga  34156  omsmeas  34157  coinflippv  34317  kur14  35044  connpconn  35063  cvmsi  35093  neibastop1  36071  neibastop2lem  36072  neibastop3  36074  onsucsuccmpi  36155  limsucncmpi  36157  bj-elpwg  36759  bj-0int  36808  bj-ismooredr  36816  lindsdom  37315  ismblfin  37362  cover2  37416  sstotbnd3  37477  heibor1  37511  heibor  37522  pclvalN  39589  pclfinN  39599  pclcmpatN  39600  dochfN  41055  elrfi  42351  cmpfiiin  42354  ismrcd2  42356  isnacs3  42367  aomclem2  42716  islssfg  42731  lmhmfgsplit  42747  lnrfg  42780  dfno2  43095  rfovcnvf1od  43671  dssmapnvod  43687  neik0pk1imk0  43714  isotone2  43716  ntrclsneine0lem  43731  ntrclsiso  43734  ntrclsk2  43735  ntrclskb  43736  ntrclsk3  43737  ntrclsk13  43738  ntrclsk4  43739  ntrneix2  43760  ntrneik13  43765  ntrrn  43789  dssmapntrcls  43795  ismnushort  43975  sspwtr  44497  sspwtrALT  44498  sspwtrALT2  44499  pwtrVD  44500  pwtrrVD  44501  sspwimp  44594  sspwimpVD  44595  sspwimpcf  44596  sspwimpcfVD  44597  sspwimpALT  44601  sspwimpALT2  44604  pwssfi  44646  ssnnf1octb  44801  dvdmsscn  45557  dvnmptconst  45562  dvnxpaek  45563  dvnmul  45564  dvnprodlem3  45569  ismbl3  45607  ismbl4  45614  stoweidlem57  45678  pwsal  45936  prsal  45939  intsal  45951  salexct  45955  issalnnd  45966  sge0rnre  45985  sge0tsms  46001  sge0cl  46002  sge0fsum  46008  sge0sup  46012  sge0less  46013  sge0gerp  46016  sge0resplit  46027  sge0split  46030  nnfoctbdj  46077  ismeannd  46088  psmeasure  46092  caragen0  46127  caragenunidm  46129  caragenuncl  46134  caragendifcl  46135  omeiunle  46138  carageniuncl  46144  caragensal  46146  caratheodorylem2  46148  0ome  46150  isomennd  46152  caragenel2d  46153  caragencmpl  46156  ovnf  46184  ovn02  46189  ovnsubaddlem1  46191  ovnsubaddlem2  46192  ovnsubadd  46193  hspmbl  46250  isvonmbl  46259  vonmblss2  46263  ovnsubadd2lem  46266  vonvolmbl  46282  nsssmfmbf  46400  smfresal  46409  smfpimbor1lem2  46420  sprsymrelfv  47066  prpair  47073  lincdifsn  47807  lcosslsp  47821  lindslinindsimp1  47840  lincresunit3lem1  47862  lincresunit3lem2  47863  lincresunit3  47864  isclatd  48309  elpglem1  48457  aacllem  48549