Theorem elpwi 4543

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  elpwid  4545  elelpwi  4546  elpwunsn  4623  elpw2g  5268  f1opw2  7618  eldifpw  7718  pwuncl  7720  iunpw  7721  mptcnfimad  7935  pwssfi  9108  f1opwfi  9263  fi0  9330  marypha1lem  9343  marypha1  9344  marypha2  9349  brwdom2  9485  brwdom3  9494  r1pwss  9706  rankpwi  9745  acndom  9971  acnnum  9972  dfac12r  10067  ackbij2lem1  10138  ackbij1lem6  10144  ackbij1b  10158  isfin2-2  10239  ssfin2  10240  enfin2i  10241  compsscnvlem  10290  compssiso  10294  fin11a  10303  enfin1ai  10304  fin12  10333  fin1a2s  10334  fin1a2  10335  hsmexlem2  10347  tskwe2  10694  inttsk  10695  inatsk  10699  indval0  12161  hashbclem  14412  pr2pwpr  14439  elss2prb  14448  qshash  15788  incexclem  15799  incexc  15800  incexc2  15801  rpnnen2lem12  16190  smupf  16445  ramval  16977  ramlb  16988  mrcflem  17570  isacs2  17617  mreacs  17622  acsfn  17623  acsfn1  17625  acsfn2  17627  sscpwex  17780  isacs3lem  18506  isacs4lem  18508  isacs5lem  18509  isacs5  18512  pmtrfrn  19431  oppglsm  19615  acsfn1p  20778  lspf  20971  pptbas  22998  clsf  23038  mretopd  23082  neiptopuni  23120  cncls2  23263  cncls  23264  cnntr  23265  restcnrm  23352  cncmp  23382  tgcmp  23391  uncmp  23393  sscmp  23395  hauscmplem  23396  cmpfi  23398  1stcrest  23443  dis2ndc  23450  lly1stc  23486  dislly  23487  comppfsc  23522  kgentopon  23528  kgen2ss  23545  kgencn  23546  kgencn2  23547  kgencn3  23548  txcmplem2  23632  txcmp  23633  tx1stc  23640  txkgen  23642  xkopt  23645  xkococnlem  23649  xkococn  23650  kqnrmlem1  23733  kqnrmlem2  23734  hmphdis  23786  isfil2  23846  isfild  23848  fbasfip  23858  neifil  23870  trfil2  23877  trufil  23900  fixufil  23912  cfinufil  23918  fin1aufil  23922  fclscmp  24020  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  ptcmplem5  24046  tgpconncompeqg  24102  imasf1oxms  24479  met2ndc  24513  zdis  24807  icccmp  24816  ovolf  25474  ismbl2  25519  cmmbl  25526  nulmbl  25527  nulmbl2  25528  unmbl  25529  shftmbl  25530  voliunlem2  25543  ioombl1  25554  uniioombl  25581  sqff1o  27170  musum  27179  nulslts  27792  nulsgts  27793  madessno  27857  oldssno  27858  newssno  27859  madebdayim  27905  eengtrkg  29080  edgssv2  29292  upgrreslem  29398  umgrreslem  29399  umgrres1lem  29404  upgrres1  29407  uhgrvd00  29628  rabfodom  32600  elpwincl1  32620  fpwrelmap  32832  esplyfval2  33756  cmpcref  34041  pcmplfinf  34052  zarclsint  34063  zarcls  34065  esumcst  34254  esumfsup  34261  esum2d  34284  dmvlsiga  34320  pwsiga  34321  sigaclci  34323  sigainb  34327  insiga  34328  pwldsys  34348  ldgenpisyslem1  34354  ldgenpisyslem3  34356  measinb  34412  measres  34413  cntmeas  34417  volmeas  34422  ddemeas  34427  dya2iocucvr  34475  sxbrsigalem1  34476  omscl  34486  omsf  34487  omsmon  34489  baselcarsg  34497  difelcarsg  34501  carsgsiga  34513  omsmeas  34514  coinflippv  34675  kur14  35451  connpconn  35470  cvmsi  35500  neibastop1  36594  neibastop2lem  36595  neibastop3  36597  onsucsuccmpi  36678  limsucncmpi  36680  bj-elpwg  37412  bj-0int  37466  bj-ismooredr  37474  lindsdom  37988  ismblfin  38035  cover2  38089  sstotbnd3  38150  heibor1  38184  heibor  38195  pclvalN  40389  pclfinN  40399  pclcmpatN  40400  dochfN  41855  elrfi  43150  cmpfiiin  43153  ismrcd2  43155  isnacs3  43166  aomclem2  43507  islssfg  43522  lmhmfgsplit  43538  lnrfg  43571  dfno2  43879  rfovcnvf1od  44455  dssmapnvod  44471  neik0pk1imk0  44498  isotone2  44500  ntrclsneine0lem  44515  ntrclsiso  44518  ntrclsk2  44519  ntrclskb  44520  ntrclsk3  44521  ntrclsk13  44522  ntrclsk4  44523  ntrneix2  44544  ntrneik13  44549  ntrrn  44573  dssmapntrcls  44579  ismnushort  44752  sspwtr  45271  sspwtrALT  45272  sspwtrALT2  45273  pwtrVD  45274  pwtrrVD  45275  sspwimp  45368  sspwimpVD  45369  sspwimpcf  45370  sspwimpcfVD  45371  sspwimpALT  45375  sspwimpALT2  45378  ssnnf1octb  45648  dvdmsscn  46386  dvnmptconst  46391  dvnxpaek  46392  dvnmul  46393  dvnprodlem3  46398  ismbl3  46436  ismbl4  46443  stoweidlem57  46507  pwsal  46765  prsal  46768  intsal  46780  salexct  46784  issalnnd  46795  sge0rnre  46814  sge0tsms  46830  sge0cl  46831  sge0fsum  46837  sge0sup  46841  sge0less  46842  sge0gerp  46845  sge0resplit  46856  sge0split  46859  nnfoctbdj  46906  ismeannd  46917  psmeasure  46921  caragen0  46956  caragenunidm  46958  caragenuncl  46963  caragendifcl  46964  omeiunle  46967  carageniuncl  46973  caragensal  46975  caratheodorylem2  46977  0ome  46979  isomennd  46981  caragenel2d  46982  caragencmpl  46985  ovnf  47013  ovn02  47018  ovnsubaddlem1  47020  ovnsubaddlem2  47021  ovnsubadd  47022  hspmbl  47079  isvonmbl  47088  vonmblss2  47092  ovnsubadd2lem  47095  vonvolmbl  47111  nsssmfmbf  47229  smfresal  47238  smfpimbor1lem2  47249  sprsymrelfv  47976  prpair  47983  grtriprop  48439  lincdifsn  48922  lcosslsp  48936  lindslinindsimp1  48955  lincresunit3lem1  48977  lincresunit3lem2  48978  lincresunit3  48979  isclatd  49480  elpglem1  50208  aacllem  50298