Theorem elpwi 4432

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

Syntax hints:   → wi 4   ∈ wcel 2050   ⊆ wss 3829  𝒫 cpw 4422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-in 3836  df-ss 3843  df-pw 4424

This theorem is referenced by:  elpwid  4434  elelpwi  4435  elpwunsn  4495  elpw2g  5103  f1opw2  7218  eldifpw  7307  iunpw  7309  f1opwfi  8623  fi0  8679  fiin  8681  marypha1lem  8692  marypha1  8693  marypha2  8698  brwdom2  8832  brwdom3  8841  r1pwss  9007  rankpwi  9046  acndom  9271  acnnum  9272  dfac12r  9366  ackbij2lem1  9439  ackbij1lem6  9445  ackbij1b  9459  isfin2-2  9539  ssfin2  9540  enfin2i  9541  compsscnvlem  9590  compssiso  9594  fin11a  9603  enfin1ai  9604  fin12  9633  fin1a2s  9634  fin1a2  9635  hsmexlem2  9647  tskwe2  9993  inttsk  9994  inatsk  9998  hashbclem  13623  pr2pwpr  13648  elss2prb  13656  qshash  15042  incexclem  15051  incexc  15052  incexc2  15053  rpnnen2lem12  15438  smupf  15687  ramval  16200  ramlb  16211  mrcflem  16735  isacs2  16782  mreacs  16787  acsfn  16788  acsfn1  16790  acsfn2  16792  sscpwex  16943  fpwipodrs  17632  isacs3lem  17634  isacs4lem  17636  isacs5lem  17637  isacs5  17640  pmtrfrn  18347  oppglsm  18528  acsfn1p  19300  lspf  19468  pptbas  21320  clsf  21360  mretopd  21404  neiptopuni  21442  cncls2  21585  cncls  21586  cnntr  21587  restcnrm  21674  cncmp  21704  tgcmp  21713  uncmp  21715  sscmp  21717  hauscmplem  21718  cmpfi  21720  1stcrest  21765  dis2ndc  21772  lly1stc  21808  dislly  21809  comppfsc  21844  kgentopon  21850  kgen2ss  21867  kgencn  21868  kgencn2  21869  kgencn3  21870  txcmplem2  21954  txcmp  21955  tx1stc  21962  txkgen  21964  xkopt  21967  xkococnlem  21971  xkococn  21972  kqnrmlem1  22055  kqnrmlem2  22056  hmphdis  22108  isfil2  22168  isfild  22170  fbasfip  22180  neifil  22192  trfil2  22199  trufil  22222  fixufil  22234  cfinufil  22240  fin1aufil  22244  fclscmp  22342  alexsubALTlem2  22360  alexsubALTlem3  22361  alexsubALTlem4  22362  ptcmplem5  22368  tgpconncompeqg  22423  imasf1oxms  22802  met2ndc  22836  zdis  23127  icccmp  23136  ovolf  23786  ismbl2  23831  cmmbl  23838  nulmbl  23839  nulmbl2  23840  unmbl  23841  shftmbl  23842  voliunlem2  23855  ioombl1  23866  uniioombl  23893  sqff1o  25461  musum  25470  eengtrkg  26475  edgssv2  26683  upgrreslem  26789  umgrreslem  26790  umgrres1lem  26795  upgrres1  26798  uhgrvd00  27019  rabfodom  30045  elpwincl1  30060  fpwrelmap  30228  cmpcref  30764  pcmplfinf  30775  esumcst  30972  esumfsup  30979  esum2d  31002  dmvlsiga  31039  pwsiga  31040  sigaclci  31042  sigainb  31046  insiga  31047  pwldsys  31067  ldgenpisyslem1  31073  ldgenpisyslem3  31075  measinb  31131  measres  31132  cntmeas  31136  volmeas  31141  ddemeas  31146  dya2iocucvr  31193  sxbrsigalem1  31194  omscl  31204  omsf  31205  omsmon  31207  baselcarsg  31215  difelcarsg  31219  carsgsiga  31231  omsmeas  31232  coinflippv  31393  kur14  32054  connpconn  32073  cvmsi  32103  nulsslt  32789  nulssgt  32790  neibastop1  33234  neibastop2lem  33235  neibastop3  33237  onsucsuccmpi  33317  limsucncmpi  33319  bj-0int  33909  bj-ismooredr  33918  lindsdom  34333  ismblfin  34380  cover2  34437  sstotbnd3  34502  heibor1  34536  heibor  34547  pclvalN  36477  pclfinN  36487  pclcmpatN  36488  dochfN  37943  elrfi  38692  cmpfiiin  38695  ismrcd2  38697  isnacs3  38708  aomclem2  39057  islssfg  39072  lmhmfgsplit  39088  lnrfg  39121  rfovcnvf1od  39719  dssmapnvod  39735  clsk1indlem3  39762  neik0pk1imk0  39766  isotone1  39767  isotone2  39768  ntrclsneine0lem  39783  ntrclsiso  39786  ntrclsk2  39787  ntrclskb  39788  ntrclsk3  39789  ntrclsk13  39790  ntrclsk4  39791  ntrneix2  39812  ntrneik13  39817  ntrrn  39841  dssmapntrcls  39847  sspwtr  40580  sspwtrALT  40581  sspwtrALT2  40582  pwtrVD  40583  pwtrrVD  40584  sspwimp  40677  sspwimpVD  40678  sspwimpcf  40679  sspwimpcfVD  40680  sspwimpALT  40684  sspwimpALT2  40687  pwssfi  40732  ssnnf1octb  40886  dvdmsscn  41657  dvnmptconst  41662  dvnxpaek  41663  dvnmul  41664  dvnprodlem3  41669  ismbl3  41708  ismbl4  41715  stoweidlem57  41779  pwsal  42037  prsal  42040  intsal  42050  salexct  42054  issalnnd  42065  sge0rnre  42083  sge0tsms  42099  sge0cl  42100  sge0fsum  42106  sge0sup  42110  sge0less  42111  sge0gerp  42114  sge0resplit  42125  sge0split  42128  nnfoctbdj  42175  ismeannd  42186  psmeasure  42190  caragen0  42225  caragenunidm  42227  caragenuncl  42232  caragendifcl  42233  omeiunle  42236  carageniuncl  42242  caragensal  42244  caratheodorylem2  42246  0ome  42248  isomennd  42250  caragenel2d  42251  caragencmpl  42254  ovnf  42282  ovn02  42287  ovnsubaddlem1  42289  ovnsubaddlem2  42290  ovnsubadd  42291  hspmbl  42348  isvonmbl  42357  vonmblss2  42361  ovnsubadd2lem  42364  vonvolmbl  42380  nsssmfmbf  42492  smfresal  42500  smfpimbor1lem2  42511  sprsymrelfv  43030  prpair  43037  isomuspgrlem2c  43369  lincdifsn  43852  lcosslsp  43866  lindslinindsimp1  43885  lincresunit3lem1  43907  lincresunit3lem2  43908  lincresunit3  43909  elpglem1  44186  aacllem  44275