Theorem elpwi 4549

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpwid  4551  elelpwi  4552  elpwunsn  4629  elpw2g  5268  f1opw2  7613  eldifpw  7713  pwuncl  7715  iunpw  7716  mptcnfimad  7930  pwssfi  9102  f1opwfi  9257  fi0  9324  marypha1lem  9337  marypha1  9338  marypha2  9343  brwdom2  9479  brwdom3  9488  r1pwss  9697  rankpwi  9736  acndom  9962  acnnum  9963  dfac12r  10058  ackbij2lem1  10129  ackbij1lem6  10135  ackbij1b  10149  isfin2-2  10230  ssfin2  10231  enfin2i  10232  compsscnvlem  10281  compssiso  10285  fin11a  10294  enfin1ai  10295  fin12  10324  fin1a2s  10325  fin1a2  10326  hsmexlem2  10338  tskwe2  10685  inttsk  10686  inatsk  10690  hashbclem  14376  pr2pwpr  14403  elss2prb  14412  qshash  15751  incexclem  15760  incexc  15761  incexc2  15762  rpnnen2lem12  16151  smupf  16406  ramval  16937  ramlb  16948  mrcflem  17530  isacs2  17577  mreacs  17582  acsfn  17583  acsfn1  17585  acsfn2  17587  sscpwex  17740  isacs3lem  18466  isacs4lem  18468  isacs5lem  18469  isacs5  18472  pmtrfrn  19391  oppglsm  19575  acsfn1p  20734  lspf  20927  pptbas  22951  clsf  22991  mretopd  23035  neiptopuni  23073  cncls2  23216  cncls  23217  cnntr  23218  restcnrm  23305  cncmp  23335  tgcmp  23344  uncmp  23346  sscmp  23348  hauscmplem  23349  cmpfi  23351  1stcrest  23396  dis2ndc  23403  lly1stc  23439  dislly  23440  comppfsc  23475  kgentopon  23481  kgen2ss  23498  kgencn  23499  kgencn2  23500  kgencn3  23501  txcmplem2  23585  txcmp  23586  tx1stc  23593  txkgen  23595  xkopt  23598  xkococnlem  23602  xkococn  23603  kqnrmlem1  23686  kqnrmlem2  23687  hmphdis  23739  isfil2  23799  isfild  23801  fbasfip  23811  neifil  23823  trfil2  23830  trufil  23853  fixufil  23865  cfinufil  23871  fin1aufil  23875  fclscmp  23973  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  ptcmplem5  23999  tgpconncompeqg  24055  imasf1oxms  24432  met2ndc  24466  zdis  24760  icccmp  24769  ovolf  25427  ismbl2  25472  cmmbl  25479  nulmbl  25480  nulmbl2  25481  unmbl  25482  shftmbl  25483  voliunlem2  25496  ioombl1  25507  uniioombl  25534  sqff1o  27132  musum  27141  nulslts  27755  nulsgts  27756  madessno  27820  oldssno  27821  newssno  27822  madebdayim  27868  eengtrkg  29043  edgssv2  29255  upgrreslem  29361  umgrreslem  29362  umgrres1lem  29367  upgrres1  29370  uhgrvd00  29592  rabfodom  32564  elpwincl1  32584  fpwrelmap  32795  esplyfval2  33714  cmpcref  34000  pcmplfinf  34011  zarclsint  34022  zarcls  34024  esumcst  34213  esumfsup  34220  esum2d  34243  dmvlsiga  34279  pwsiga  34280  sigaclci  34282  sigainb  34286  insiga  34287  pwldsys  34307  ldgenpisyslem1  34313  ldgenpisyslem3  34315  measinb  34371  measres  34372  cntmeas  34376  volmeas  34381  ddemeas  34386  dya2iocucvr  34434  sxbrsigalem1  34435  omscl  34445  omsf  34446  omsmon  34448  baselcarsg  34456  difelcarsg  34460  carsgsiga  34472  omsmeas  34473  coinflippv  34634  kur14  35404  connpconn  35423  cvmsi  35453  neibastop1  36547  neibastop2lem  36548  neibastop3  36550  onsucsuccmpi  36631  limsucncmpi  36633  bj-elpwg  37357  bj-0int  37411  bj-ismooredr  37419  lindsdom  37926  ismblfin  37973  cover2  38027  sstotbnd3  38088  heibor1  38122  heibor  38133  pclvalN  40327  pclfinN  40337  pclcmpatN  40338  dochfN  41793  elrfi  43125  cmpfiiin  43128  ismrcd2  43130  isnacs3  43141  aomclem2  43486  islssfg  43501  lmhmfgsplit  43517  lnrfg  43550  dfno2  43858  rfovcnvf1od  44434  dssmapnvod  44450  neik0pk1imk0  44477  isotone2  44479  ntrclsneine0lem  44494  ntrclsiso  44497  ntrclsk2  44498  ntrclskb  44499  ntrclsk3  44500  ntrclsk13  44501  ntrclsk4  44502  ntrneix2  44523  ntrneik13  44528  ntrrn  44552  dssmapntrcls  44558  ismnushort  44731  sspwtr  45250  sspwtrALT  45251  sspwtrALT2  45252  pwtrVD  45253  pwtrrVD  45254  sspwimp  45347  sspwimpVD  45348  sspwimpcf  45349  sspwimpcfVD  45350  sspwimpALT  45354  sspwimpALT2  45357  ssnnf1octb  45627  dvdmsscn  46368  dvnmptconst  46373  dvnxpaek  46374  dvnmul  46375  dvnprodlem3  46380  ismbl3  46418  ismbl4  46425  stoweidlem57  46489  pwsal  46747  prsal  46750  intsal  46762  salexct  46766  issalnnd  46777  sge0rnre  46796  sge0tsms  46812  sge0cl  46813  sge0fsum  46819  sge0sup  46823  sge0less  46824  sge0gerp  46827  sge0resplit  46838  sge0split  46841  nnfoctbdj  46888  ismeannd  46899  psmeasure  46903  caragen0  46938  caragenunidm  46940  caragenuncl  46945  caragendifcl  46946  omeiunle  46949  carageniuncl  46955  caragensal  46957  caratheodorylem2  46959  0ome  46961  isomennd  46963  caragenel2d  46964  caragencmpl  46967  ovnf  46995  ovn02  47000  ovnsubaddlem1  47002  ovnsubaddlem2  47003  ovnsubadd  47004  hspmbl  47061  isvonmbl  47070  vonmblss2  47074  ovnsubadd2lem  47077  vonvolmbl  47093  nsssmfmbf  47211  smfresal  47220  smfpimbor1lem2  47231  sprsymrelfv  47928  prpair  47935  grtriprop  48375  lincdifsn  48858  lcosslsp  48872  lindslinindsimp1  48891  lincresunit3lem1  48913  lincresunit3lem2  48914  lincresunit3  48915  isclatd  49416  elpglem1  50144  aacllem  50234