Theorem elpwi 4565

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

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-pw 4560

This theorem is referenced by:  elpwid  4567  elelpwi  4568  elpwunsn  4646  elpw2g  5294  f1opw2  7655  eldifpw  7755  pwuncl  7757  iunpw  7758  mptcnfimad  7971  pwssfi  9149  f1opwfi  9301  fi0  9368  marypha1lem  9381  marypha1  9382  marypha2  9387  brwdom2  9523  brwdom3  9532  r1pwss  9744  rankpwi  9783  acndom  10023  acnnum  10024  dfac12r  10118  ackbij2lem1  10189  ackbij1lem6  10195  ackbij1b  10209  isfin2-2  10291  ssfin2  10292  enfin2i  10293  compsscnvlem  10342  compssiso  10346  fin11a  10355  enfin1ai  10356  fin12  10385  fin1a2s  10386  fin1a2  10387  hsmexlem2  10399  tskwe2  10746  inttsk  10747  inatsk  10751  indval0  12213  hashbclem  14479  pr2pwpr  14506  elss2prb  14515  qshash  15869  incexclem  15880  incexc  15881  incexc2  15882  rpnnen2lem12  16271  smupf  16526  ramval  17058  ramlb  17069  mrcflem  17652  isacs2  17699  mreacs  17704  acsfn  17705  acsfn1  17707  acsfn2  17709  sscpwex  17862  isacs3lem  18588  isacs4lem  18590  isacs5lem  18591  isacs5  18594  pmtrfrn  19519  oppglsm  19703  acsfn1p  20871  lspf  21064  pptbas  23126  clsf  23166  mretopd  23210  neiptopuni  23248  cncls2  23391  cncls  23392  cnntr  23393  restcnrm  23480  cncmp  23510  tgcmp  23519  uncmp  23521  sscmp  23523  hauscmplem  23524  cmpfi  23526  1stcrest  23571  dis2ndc  23578  lly1stc  23614  dislly  23615  comppfsc  23650  kgentopon  23656  kgen2ss  23673  kgencn  23674  kgencn2  23675  kgencn3  23676  txcmplem2  23760  txcmp  23761  tx1stc  23768  txkgen  23770  xkopt  23773  xkococnlem  23777  xkococn  23778  kqnrmlem1  23861  kqnrmlem2  23862  hmphdis  23914  isfil2  23974  isfild  23976  fbasfip  23986  neifil  23998  trfil2  24005  trufil  24028  fixufil  24040  cfinufil  24046  fin1aufil  24050  fclscmp  24148  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALTlem4  24168  ptcmplem5  24174  tgpconncompeqg  24230  imasf1oxms  24607  met2ndc  24641  zdis  24935  icccmp  24944  ovolf  25602  ismbl2  25647  cmmbl  25654  nulmbl  25655  nulmbl2  25656  unmbl  25657  shftmbl  25658  voliunlem2  25671  ioombl1  25682  uniioombl  25709  sqff1o  27304  musum  27313  nulslts  27926  nulsgts  27927  madessno  27991  oldssno  27992  newssno  27993  madebdayim  28039  eengtrkg  29245  edgssv2  29457  upgrreslem  29563  umgrreslem  29564  umgrres1lem  29569  upgrres1  29572  uhgrvd00  29793  rabfodom  32761  elpwincl1  32781  fpwrelmap  32990  esplyfval2  33872  cmpcref  34157  pcmplfinf  34168  zarclsint  34179  zarcls  34181  esumcst  34370  esumfsup  34377  esum2d  34400  dmvlsiga  34436  pwsiga  34437  sigaclci  34439  sigainb  34443  insiga  34444  pwldsys  34464  ldgenpisyslem1  34470  ldgenpisyslem3  34472  measinb  34528  measres  34529  cntmeas  34533  volmeas  34538  ddemeas  34543  dya2iocucvr  34591  sxbrsigalem1  34592  omscl  34602  omsf  34603  omsmon  34605  baselcarsg  34613  difelcarsg  34617  carsgsiga  34629  omsmeas  34630  coinflippv  34791  kur14  35579  connpconn  35598  cvmsi  35628  neibastop1  36732  neibastop2lem  36733  neibastop3  36735  onsucsuccmpi  36816  limsucncmpi  36818  bj-elpwg  37549  bj-0int  37603  bj-ismooredr  37611  lindsdom  38125  ismblfin  38172  cover2  38226  sstotbnd3  38287  heibor1  38321  heibor  38332  pclvalN  40526  pclfinN  40536  pclcmpatN  40537  dochfN  41992  elrfi  43287  cmpfiiin  43290  ismrcd2  43292  isnacs3  43303  aomclem2  43644  islssfg  43659  lmhmfgsplit  43675  lnrfg  43708  dfno2  44016  rfovcnvf1od  44592  dssmapnvod  44608  neik0pk1imk0  44635  isotone2  44637  ntrclsneine0lem  44652  ntrclsiso  44655  ntrclsk2  44656  ntrclskb  44657  ntrclsk3  44658  ntrclsk13  44659  ntrclsk4  44660  ntrneix2  44681  ntrneik13  44686  ntrrn  44710  dssmapntrcls  44716  ismnushort  44875  sspwtr  45394  sspwtrALT  45395  sspwtrALT2  45396  pwtrVD  45397  pwtrrVD  45398  sspwimp  45491  sspwimpVD  45492  sspwimpcf  45493  sspwimpcfVD  45494  sspwimpALT  45498  sspwimpALT2  45501  ssnnf1octb  45770  dvdmsscn  46508  dvnmptconst  46513  dvnxpaek  46514  dvnmul  46515  dvnprodlem3  46520  ismbl3  46558  ismbl4  46565  stoweidlem57  46629  pwsal  46887  prsal  46890  intsal  46902  salexct  46906  issalnnd  46917  sge0rnre  46936  sge0tsms  46952  sge0cl  46953  sge0fsum  46959  sge0sup  46963  sge0less  46964  sge0gerp  46967  sge0resplit  46978  sge0split  46981  nnfoctbdj  47028  ismeannd  47039  psmeasure  47043  caragen0  47078  caragenunidm  47080  caragenuncl  47085  caragendifcl  47086  omeiunle  47089  carageniuncl  47095  caragensal  47097  caratheodorylem2  47099  0ome  47101  isomennd  47103  caragenel2d  47104  caragencmpl  47107  ovnf  47135  ovn02  47140  ovnsubaddlem1  47142  ovnsubaddlem2  47143  ovnsubadd  47144  hspmbl  47201  isvonmbl  47210  vonmblss2  47214  ovnsubadd2lem  47217  vonvolmbl  47233  nsssmfmbf  47351  smfresal  47360  smfpimbor1lem2  47371  sprsymrelfv  48098  prpair  48105  grtriprop  48561  lincdifsn  49055  lcosslsp  49069  lindslinindsimp1  49088  lincresunit3lem1  49110  lincresunit3lem2  49111  lincresunit3  49112  isclatd  49612  elpglem1  50340  aacllem  50430