Theorem elpwi 4609

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3948  𝒫 cpw 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  elpwid  4611  elelpwi  4612  elpwunsn  4687  elpw2g  5344  f1opw2  7658  eldifpw  7752  pwuncl  7754  iunpw  7755  f1opwfi  9353  fi0  9412  marypha1lem  9425  marypha1  9426  marypha2  9431  brwdom2  9565  brwdom3  9574  r1pwss  9776  rankpwi  9815  acndom  10043  acnnum  10044  dfac12r  10138  ackbij2lem1  10211  ackbij1lem6  10217  ackbij1b  10231  isfin2-2  10311  ssfin2  10312  enfin2i  10313  compsscnvlem  10362  compssiso  10366  fin11a  10375  enfin1ai  10376  fin12  10405  fin1a2s  10406  fin1a2  10407  hsmexlem2  10419  tskwe2  10765  inttsk  10766  inatsk  10770  hashbclem  14408  pr2pwpr  14437  elss2prb  14445  qshash  15770  incexclem  15779  incexc  15780  incexc2  15781  rpnnen2lem12  16165  smupf  16416  ramval  16938  ramlb  16949  mrcflem  17547  isacs2  17594  mreacs  17599  acsfn  17600  acsfn1  17602  acsfn2  17604  sscpwex  17759  isacs3lem  18492  isacs4lem  18494  isacs5lem  18495  isacs5  18498  pmtrfrn  19321  oppglsm  19505  acsfn1p  20408  lspf  20578  pptbas  22503  clsf  22544  mretopd  22588  neiptopuni  22626  cncls2  22769  cncls  22770  cnntr  22771  restcnrm  22858  cncmp  22888  tgcmp  22897  uncmp  22899  sscmp  22901  hauscmplem  22902  cmpfi  22904  1stcrest  22949  dis2ndc  22956  lly1stc  22992  dislly  22993  comppfsc  23028  kgentopon  23034  kgen2ss  23051  kgencn  23052  kgencn2  23053  kgencn3  23054  txcmplem2  23138  txcmp  23139  tx1stc  23146  txkgen  23148  xkopt  23151  xkococnlem  23155  xkococn  23156  kqnrmlem1  23239  kqnrmlem2  23240  hmphdis  23292  isfil2  23352  isfild  23354  fbasfip  23364  neifil  23376  trfil2  23383  trufil  23406  fixufil  23418  cfinufil  23424  fin1aufil  23428  fclscmp  23526  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  ptcmplem5  23552  tgpconncompeqg  23608  imasf1oxms  23990  met2ndc  24024  zdis  24324  icccmp  24333  ovolf  24991  ismbl2  25036  cmmbl  25043  nulmbl  25044  nulmbl2  25045  unmbl  25046  shftmbl  25047  voliunlem2  25060  ioombl1  25071  uniioombl  25098  sqff1o  26676  musum  26685  nulsslt  27288  nulssgt  27289  madessno  27345  oldssno  27346  newssno  27347  madebdayim  27372  eengtrkg  28234  edgssv2  28445  upgrreslem  28551  umgrreslem  28552  umgrres1lem  28557  upgrres1  28560  uhgrvd00  28781  rabfodom  31731  elpwincl1  31751  fpwrelmap  31946  cmpcref  32819  pcmplfinf  32830  zarclsint  32841  zarcls  32843  esumcst  33050  esumfsup  33057  esum2d  33080  dmvlsiga  33116  pwsiga  33117  sigaclci  33119  sigainb  33123  insiga  33124  pwldsys  33144  ldgenpisyslem1  33150  ldgenpisyslem3  33152  measinb  33208  measres  33209  cntmeas  33213  volmeas  33218  ddemeas  33223  dya2iocucvr  33272  sxbrsigalem1  33273  omscl  33283  omsf  33284  omsmon  33286  baselcarsg  33294  difelcarsg  33298  carsgsiga  33310  omsmeas  33311  coinflippv  33471  kur14  34196  connpconn  34215  cvmsi  34245  neibastop1  35233  neibastop2lem  35234  neibastop3  35236  onsucsuccmpi  35317  limsucncmpi  35319  bj-elpwg  35922  bj-0int  35971  bj-ismooredr  35979  lindsdom  36471  ismblfin  36518  cover2  36572  sstotbnd3  36633  heibor1  36667  heibor  36678  pclvalN  38750  pclfinN  38760  pclcmpatN  38761  dochfN  40216  elrfi  41418  cmpfiiin  41421  ismrcd2  41423  isnacs3  41434  aomclem2  41783  islssfg  41798  lmhmfgsplit  41814  lnrfg  41847  dfno2  42165  rfovcnvf1od  42741  dssmapnvod  42757  neik0pk1imk0  42784  isotone2  42786  ntrclsneine0lem  42801  ntrclsiso  42804  ntrclsk2  42805  ntrclskb  42806  ntrclsk3  42807  ntrclsk13  42808  ntrclsk4  42809  ntrneix2  42830  ntrneik13  42835  ntrrn  42859  dssmapntrcls  42865  ismnushort  43046  sspwtr  43568  sspwtrALT  43569  sspwtrALT2  43570  pwtrVD  43571  pwtrrVD  43572  sspwimp  43665  sspwimpVD  43666  sspwimpcf  43667  sspwimpcfVD  43668  sspwimpALT  43672  sspwimpALT2  43675  pwssfi  43718  ssnnf1octb  43879  dvdmsscn  44639  dvnmptconst  44644  dvnxpaek  44645  dvnmul  44646  dvnprodlem3  44651  ismbl3  44689  ismbl4  44696  stoweidlem57  44760  pwsal  45018  prsal  45021  intsal  45033  salexct  45037  issalnnd  45048  sge0rnre  45067  sge0tsms  45083  sge0cl  45084  sge0fsum  45090  sge0sup  45094  sge0less  45095  sge0gerp  45098  sge0resplit  45109  sge0split  45112  nnfoctbdj  45159  ismeannd  45170  psmeasure  45174  caragen0  45209  caragenunidm  45211  caragenuncl  45216  caragendifcl  45217  omeiunle  45220  carageniuncl  45226  caragensal  45228  caratheodorylem2  45230  0ome  45232  isomennd  45234  caragenel2d  45235  caragencmpl  45238  ovnf  45266  ovn02  45271  ovnsubaddlem1  45273  ovnsubaddlem2  45274  ovnsubadd  45275  hspmbl  45332  isvonmbl  45341  vonmblss2  45345  ovnsubadd2lem  45348  vonvolmbl  45364  nsssmfmbf  45482  smfresal  45491  smfpimbor1lem2  45502  sprsymrelfv  46149  prpair  46156  isomuspgrlem2c  46485  lincdifsn  47059  lcosslsp  47073  lindslinindsimp1  47092  lincresunit3lem1  47114  lincresunit3lem2  47115  lincresunit3  47116  isclatd  47562  elpglem1  47710  aacllem  47802