Theorem elpwi 4570

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-pw 4565

This theorem is referenced by:  elpwid  4572  elelpwi  4573  elpwunsn  4648  elpw2g  5288  f1opw2  7644  eldifpw  7744  pwuncl  7746  iunpw  7747  mptcnfimad  7965  pwssfi  9141  f1opwfi  9307  fi0  9371  marypha1lem  9384  marypha1  9385  marypha2  9390  brwdom2  9526  brwdom3  9535  r1pwss  9737  rankpwi  9776  acndom  10004  acnnum  10005  dfac12r  10100  ackbij2lem1  10171  ackbij1lem6  10177  ackbij1b  10191  isfin2-2  10272  ssfin2  10273  enfin2i  10274  compsscnvlem  10323  compssiso  10327  fin11a  10336  enfin1ai  10337  fin12  10366  fin1a2s  10367  fin1a2  10368  hsmexlem2  10380  tskwe2  10726  inttsk  10727  inatsk  10731  hashbclem  14417  pr2pwpr  14444  elss2prb  14453  qshash  15793  incexclem  15802  incexc  15803  incexc2  15804  rpnnen2lem12  16193  smupf  16448  ramval  16979  ramlb  16990  mrcflem  17567  isacs2  17614  mreacs  17619  acsfn  17620  acsfn1  17622  acsfn2  17624  sscpwex  17777  isacs3lem  18501  isacs4lem  18503  isacs5lem  18504  isacs5  18507  pmtrfrn  19388  oppglsm  19572  acsfn1p  20708  lspf  20880  pptbas  22895  clsf  22935  mretopd  22979  neiptopuni  23017  cncls2  23160  cncls  23161  cnntr  23162  restcnrm  23249  cncmp  23279  tgcmp  23288  uncmp  23290  sscmp  23292  hauscmplem  23293  cmpfi  23295  1stcrest  23340  dis2ndc  23347  lly1stc  23383  dislly  23384  comppfsc  23419  kgentopon  23425  kgen2ss  23442  kgencn  23443  kgencn2  23444  kgencn3  23445  txcmplem2  23529  txcmp  23530  tx1stc  23537  txkgen  23539  xkopt  23542  xkococnlem  23546  xkococn  23547  kqnrmlem1  23630  kqnrmlem2  23631  hmphdis  23683  isfil2  23743  isfild  23745  fbasfip  23755  neifil  23767  trfil2  23774  trufil  23797  fixufil  23809  cfinufil  23815  fin1aufil  23819  fclscmp  23917  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem5  23943  tgpconncompeqg  23999  imasf1oxms  24377  met2ndc  24411  zdis  24705  icccmp  24714  ovolf  25383  ismbl2  25428  cmmbl  25435  nulmbl  25436  nulmbl2  25437  unmbl  25438  shftmbl  25439  voliunlem2  25452  ioombl1  25463  uniioombl  25490  sqff1o  27092  musum  27101  nulsslt  27709  nulssgt  27710  madessno  27768  oldssno  27769  newssno  27770  madebdayim  27799  eengtrkg  28913  edgssv2  29125  upgrreslem  29231  umgrreslem  29232  umgrres1lem  29237  upgrres1  29240  uhgrvd00  29462  rabfodom  32434  elpwincl1  32454  fpwrelmap  32656  cmpcref  33840  pcmplfinf  33851  zarclsint  33862  zarcls  33864  esumcst  34053  esumfsup  34060  esum2d  34083  dmvlsiga  34119  pwsiga  34120  sigaclci  34122  sigainb  34126  insiga  34127  pwldsys  34147  ldgenpisyslem1  34153  ldgenpisyslem3  34155  measinb  34211  measres  34212  cntmeas  34216  volmeas  34221  ddemeas  34226  dya2iocucvr  34275  sxbrsigalem1  34276  omscl  34286  omsf  34287  omsmon  34289  baselcarsg  34297  difelcarsg  34301  carsgsiga  34313  omsmeas  34314  coinflippv  34475  kur14  35203  connpconn  35222  cvmsi  35252  neibastop1  36347  neibastop2lem  36348  neibastop3  36350  onsucsuccmpi  36431  limsucncmpi  36433  bj-elpwg  37040  bj-0int  37089  bj-ismooredr  37097  lindsdom  37608  ismblfin  37655  cover2  37709  sstotbnd3  37770  heibor1  37804  heibor  37815  pclvalN  39884  pclfinN  39894  pclcmpatN  39895  dochfN  41350  elrfi  42682  cmpfiiin  42685  ismrcd2  42687  isnacs3  42698  aomclem2  43044  islssfg  43059  lmhmfgsplit  43075  lnrfg  43108  dfno2  43417  rfovcnvf1od  43993  dssmapnvod  44009  neik0pk1imk0  44036  isotone2  44038  ntrclsneine0lem  44053  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneix2  44082  ntrneik13  44087  ntrrn  44111  dssmapntrcls  44117  ismnushort  44290  sspwtr  44810  sspwtrALT  44811  sspwtrALT2  44812  pwtrVD  44813  pwtrrVD  44814  sspwimp  44907  sspwimpVD  44908  sspwimpcf  44909  sspwimpcfVD  44910  sspwimpALT  44914  sspwimpALT2  44917  ssnnf1octb  45188  dvdmsscn  45934  dvnmptconst  45939  dvnxpaek  45940  dvnmul  45941  dvnprodlem3  45946  ismbl3  45984  ismbl4  45991  stoweidlem57  46055  pwsal  46313  prsal  46316  intsal  46328  salexct  46332  issalnnd  46343  sge0rnre  46362  sge0tsms  46378  sge0cl  46379  sge0fsum  46385  sge0sup  46389  sge0less  46390  sge0gerp  46393  sge0resplit  46404  sge0split  46407  nnfoctbdj  46454  ismeannd  46465  psmeasure  46469  caragen0  46504  caragenunidm  46506  caragenuncl  46511  caragendifcl  46512  omeiunle  46515  carageniuncl  46521  caragensal  46523  caratheodorylem2  46525  0ome  46527  isomennd  46529  caragenel2d  46530  caragencmpl  46533  ovnf  46561  ovn02  46566  ovnsubaddlem1  46568  ovnsubaddlem2  46569  ovnsubadd  46570  hspmbl  46627  isvonmbl  46636  vonmblss2  46640  ovnsubadd2lem  46643  vonvolmbl  46659  nsssmfmbf  46777  smfresal  46786  smfpimbor1lem2  46797  sprsymrelfv  47495  prpair  47502  grtriprop  47940  lincdifsn  48413  lcosslsp  48427  lindslinindsimp1  48446  lincresunit3lem1  48468  lincresunit3lem2  48469  lincresunit3  48470  isclatd  48971  elpglem1  49700  aacllem  49790