Theorem elpwi 4561

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-pw 4556

This theorem is referenced by:  elpwid  4563  elelpwi  4564  elpwunsn  4641  elpw2g  5278  f1opw2  7613  eldifpw  7713  pwuncl  7715  iunpw  7716  mptcnfimad  7930  pwssfi  9101  f1opwfi  9256  fi0  9323  marypha1lem  9336  marypha1  9337  marypha2  9342  brwdom2  9478  brwdom3  9487  r1pwss  9696  rankpwi  9735  acndom  9961  acnnum  9962  dfac12r  10057  ackbij2lem1  10128  ackbij1lem6  10134  ackbij1b  10148  isfin2-2  10229  ssfin2  10230  enfin2i  10231  compsscnvlem  10280  compssiso  10284  fin11a  10293  enfin1ai  10294  fin12  10323  fin1a2s  10324  fin1a2  10325  hsmexlem2  10337  tskwe2  10684  inttsk  10685  inatsk  10689  hashbclem  14375  pr2pwpr  14402  elss2prb  14411  qshash  15750  incexclem  15759  incexc  15760  incexc2  15761  rpnnen2lem12  16150  smupf  16405  ramval  16936  ramlb  16947  mrcflem  17529  isacs2  17576  mreacs  17581  acsfn  17582  acsfn1  17584  acsfn2  17586  sscpwex  17739  isacs3lem  18465  isacs4lem  18467  isacs5lem  18468  isacs5  18471  pmtrfrn  19387  oppglsm  19571  acsfn1p  20732  lspf  20925  pptbas  22952  clsf  22992  mretopd  23036  neiptopuni  23074  cncls2  23217  cncls  23218  cnntr  23219  restcnrm  23306  cncmp  23336  tgcmp  23345  uncmp  23347  sscmp  23349  hauscmplem  23350  cmpfi  23352  1stcrest  23397  dis2ndc  23404  lly1stc  23440  dislly  23441  comppfsc  23476  kgentopon  23482  kgen2ss  23499  kgencn  23500  kgencn2  23501  kgencn3  23502  txcmplem2  23586  txcmp  23587  tx1stc  23594  txkgen  23596  xkopt  23599  xkococnlem  23603  xkococn  23604  kqnrmlem1  23687  kqnrmlem2  23688  hmphdis  23740  isfil2  23800  isfild  23802  fbasfip  23812  neifil  23824  trfil2  23831  trufil  23854  fixufil  23866  cfinufil  23872  fin1aufil  23876  fclscmp  23974  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  ptcmplem5  24000  tgpconncompeqg  24056  imasf1oxms  24433  met2ndc  24467  zdis  24761  icccmp  24770  ovolf  25439  ismbl2  25484  cmmbl  25491  nulmbl  25492  nulmbl2  25493  unmbl  25494  shftmbl  25495  voliunlem2  25508  ioombl1  25519  uniioombl  25546  sqff1o  27148  musum  27157  nulslts  27771  nulsgts  27772  madessno  27836  oldssno  27837  newssno  27838  madebdayim  27884  eengtrkg  29059  edgssv2  29271  upgrreslem  29377  umgrreslem  29378  umgrres1lem  29383  upgrres1  29386  uhgrvd00  29608  rabfodom  32580  elpwincl1  32600  fpwrelmap  32812  esplyfval2  33723  cmpcref  34007  pcmplfinf  34018  zarclsint  34029  zarcls  34031  esumcst  34220  esumfsup  34227  esum2d  34250  dmvlsiga  34286  pwsiga  34287  sigaclci  34289  sigainb  34293  insiga  34294  pwldsys  34314  ldgenpisyslem1  34320  ldgenpisyslem3  34322  measinb  34378  measres  34379  cntmeas  34383  volmeas  34388  ddemeas  34393  dya2iocucvr  34441  sxbrsigalem1  34442  omscl  34452  omsf  34453  omsmon  34455  baselcarsg  34463  difelcarsg  34467  carsgsiga  34479  omsmeas  34480  coinflippv  34641  kur14  35410  connpconn  35429  cvmsi  35459  neibastop1  36553  neibastop2lem  36554  neibastop3  36556  onsucsuccmpi  36637  limsucncmpi  36639  bj-elpwg  37253  bj-0int  37302  bj-ismooredr  37310  lindsdom  37811  ismblfin  37858  cover2  37912  sstotbnd3  37973  heibor1  38007  heibor  38018  pclvalN  40146  pclfinN  40156  pclcmpatN  40157  dochfN  41612  elrfi  42932  cmpfiiin  42935  ismrcd2  42937  isnacs3  42948  aomclem2  43293  islssfg  43308  lmhmfgsplit  43324  lnrfg  43357  dfno2  43665  rfovcnvf1od  44241  dssmapnvod  44257  neik0pk1imk0  44284  isotone2  44286  ntrclsneine0lem  44301  ntrclsiso  44304  ntrclsk2  44305  ntrclskb  44306  ntrclsk3  44307  ntrclsk13  44308  ntrclsk4  44309  ntrneix2  44330  ntrneik13  44335  ntrrn  44359  dssmapntrcls  44365  ismnushort  44538  sspwtr  45057  sspwtrALT  45058  sspwtrALT2  45059  pwtrVD  45060  pwtrrVD  45061  sspwimp  45154  sspwimpVD  45155  sspwimpcf  45156  sspwimpcfVD  45157  sspwimpALT  45161  sspwimpALT2  45164  ssnnf1octb  45434  dvdmsscn  46176  dvnmptconst  46181  dvnxpaek  46182  dvnmul  46183  dvnprodlem3  46188  ismbl3  46226  ismbl4  46233  stoweidlem57  46297  pwsal  46555  prsal  46558  intsal  46570  salexct  46574  issalnnd  46585  sge0rnre  46604  sge0tsms  46620  sge0cl  46621  sge0fsum  46627  sge0sup  46631  sge0less  46632  sge0gerp  46635  sge0resplit  46646  sge0split  46649  nnfoctbdj  46696  ismeannd  46707  psmeasure  46711  caragen0  46746  caragenunidm  46748  caragenuncl  46753  caragendifcl  46754  omeiunle  46757  carageniuncl  46763  caragensal  46765  caratheodorylem2  46767  0ome  46769  isomennd  46771  caragenel2d  46772  caragencmpl  46775  ovnf  46803  ovn02  46808  ovnsubaddlem1  46810  ovnsubaddlem2  46811  ovnsubadd  46812  hspmbl  46869  isvonmbl  46878  vonmblss2  46882  ovnsubadd2lem  46885  vonvolmbl  46901  nsssmfmbf  47019  smfresal  47028  smfpimbor1lem2  47039  sprsymrelfv  47736  prpair  47743  grtriprop  48183  lincdifsn  48666  lcosslsp  48680  lindslinindsimp1  48699  lincresunit3lem1  48721  lincresunit3lem2  48722  lincresunit3  48723  isclatd  49224  elpglem1  49952  aacllem  50042