Theorem elpwi 4567

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-pw 4562

This theorem is used by:  elpwid  4569  elelpwi  4570  elpwunsn  4645  elpw2g  5299  f1opw2  7700  eldifpw  7806  pwuncl  7808  iunpw  7809  mptcnfimad  8022  pwssfi  9220  f1opwfi  9373  fi0  9439  marypha1lem  9452  marypha1  9453  marypha2  9458  brwdom2  9594  brwdom3  9603  r1pwss  9818  rankpwi  9859  acndom  10157  acnnum  10158  dfac12r  10252  ackbij2lem1  10323  ackbij1lem6  10329  ackbij1b  10343  isfin2-2  10424  ssfin2  10425  enfin2i  10426  compsscnvlem  10475  compssiso  10479  fin11a  10488  enfin1ai  10489  fin12  10518  fin1a2s  10519  fin1a2  10520  hsmexlem2  10532  tskwe2  10885  inttsk  10886  inatsk  10890  indval0  12351  hashbclem  14624  pr2pwpr  14651  elss2prb  14660  qshash  16023  incexclem  16034  incexc  16035  incexc2  16036  rpnnen2lem12  16422  smupf  16677  ramval  17215  ramlb  17226  mrcflem  17809  isacs2  17856  mreacs  17861  acsfn  17862  acsfn1  17864  acsfn2  17866  sscpwex  18019  isacs3lem  18745  isacs4lem  18747  isacs5lem  18748  isacs5  18751  pmtrfrn  19702  oppglsm  19886  acsfn1p  21086  lspf  21279  lindsdom  22186  pptbas  23356  clsf  23396  mretopd  23440  neiptopuni  23478  cncls2  23621  cncls  23622  cnntr  23623  restcnrm  23710  cncmp  23740  tgcmp  23749  uncmp  23751  sscmp  23753  hauscmplem  23754  cmpfi  23756  1stcrest  23801  dis2ndc  23809  lly1stc  23845  dislly  23846  comppfsc  23881  kgentopon  23887  kgen2ss  23904  kgencn  23905  kgencn2  23906  kgencn3  23907  txcmplem2  23991  txcmp  23992  tx1stc  23999  txkgen  24001  xkopt  24004  xkococnlem  24008  xkococn  24009  kqnrmlem1  24092  kqnrmlem2  24093  hmphdis  24145  isfil2  24205  isfild  24207  fbasfip  24217  neifil  24229  trfil2  24236  trufil  24259  fixufil  24271  cfinufil  24277  fin1aufil  24281  fclscmp  24379  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALTlem4  24399  ptcmplem5  24405  tgpconncompeqg  24461  imasf1oxms  24838  met2ndc  24872  zdis  25166  icccmp  25175  ovolf  25833  ismbl2  25878  cmmbl  25885  nulmbl  25886  nulmbl2  25887  unmbl  25888  shftmbl  25889  voliunlem2  25902  ioombl1  25913  uniioombl  25940  sqff1o  27539  musum  27548  nulslts  28191  nulsgts  28192  madessno  28256  oldssno  28257  newssno  28258  madebdayim  28304  eengtrkg  29594  edgssv2  29809  upgrreslem  29915  umgrreslem  29916  umgrres1lem  29921  upgrres1  29924  uhgrvd00  30145  rabfodom  33173  elpwincl1  33193  fpwrelmap  33395  esplyfval2  34267  cmpcref  34552  pcmplfinf  34563  zarclsint  34574  zarcls  34576  esumcst  34765  esumfsup  34772  esum2d  34795  dmvlsiga  34831  pwsiga  34832  sigaclci  34834  sigainb  34839  insiga  34840  pwldsys  34860  ldgenpisyslem1  34866  ldgenpisyslem3  34868  measinb  34924  measres  34925  cntmeas  34929  volmeas  34934  ddemeas  34939  dya2iocucvr  34986  sxbrsigalem1  34987  omscl  34997  omsf  34998  omsmon  35000  baselcarsg  35008  difelcarsg  35012  carsgsiga  35024  omsmeas  35025  coinflippv  35186  kur14  36148  connpconn  36167  cvmsi  36197  neibastop1  37325  neibastop2lem  37326  neibastop3  37328  onsucsuccmpi  37409  limsucncmpi  37411  bj-elpwg  38158  bj-0int  38213  bj-ismooredr  38221  ismblfin  38771  cover2  38841  sstotbnd3  38902  heibor1  38936  heibor  38947  pclvalN  41139  pclfinN  41149  pclcmpatN  41150  dochfN  42605  elrfi  43898  cmpfiiin  43901  ismrcd2  43903  isnacs3  43914  aomclem2  44250  islssfg  44265  lmhmfgsplit  44281  lnrfg  44313  dfno2  44621  rfovcnvf1od  45196  dssmapnvod  45212  neik0pk1imk0  45239  isotone2  45241  ntrclsneine0lem  45256  ntrclsiso  45259  ntrclsk2  45260  ntrclskb  45261  ntrclsk3  45262  ntrclsk13  45263  ntrclsk4  45264  ntrneix2  45285  ntrneik13  45290  ntrrn  45314  dssmapntrcls  45320  ismnushort  45477  sspwtr  45994  sspwtrALT  45995  sspwtrALT2  45996  pwtrVD  45997  pwtrrVD  45998  sspwimp  46091  sspwimpVD  46092  sspwimpcf  46093  sspwimpcfVD  46094  sspwimpALT  46098  sspwimpALT2  46101  ssnnf1octb  46414  dvdmsscn  47151  dvnmptconst  47156  dvnxpaek  47157  dvnmul  47158  dvnprodlem3  47163  ismbl3  47201  ismbl4  47208  stoweidlem57  47272  pwsal  47530  prsal  47533  intsal  47545  salexct  47549  issalnnd  47560  sge0rnre  47579  sge0tsms  47595  sge0cl  47596  sge0fsum  47602  sge0sup  47606  sge0less  47607  sge0gerp  47610  sge0resplit  47621  sge0split  47624  nnfoctbdj  47671  ismeannd  47682  psmeasure  47686  caragen0  47721  caragenunidm  47723  caragenuncl  47728  caragendifcl  47729  omeiunle  47732  carageniuncl  47738  caragensal  47740  caratheodorylem2  47742  0ome  47744  isomennd  47746  caragenel2d  47747  caragencmpl  47750  ovnf  47778  ovn02  47783  ovnsubaddlem1  47785  ovnsubaddlem2  47786  ovnsubadd  47787  hspmbl  47844  isvonmbl  47853  vonmblss2  47857  ovnsubadd2lem  47860  vonvolmbl  47876  nsssmfmbf  47994  smfresal  48003  smfpimbor1lem2  48014  sprsymrelfv  48781  prpair  48788  grtriprop  49244  lincdifsn  49741  lcosslsp  49755  lindslinindsimp1  49774  lincresunit3lem1  49796  lincresunit3lem2  49797  lincresunit3  49798  itscnhlinecirc02p  50102  isclatd  50302  elpglem1  51084  aacllem  51219