Theorem elpwi 4607

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  𝒫 cpw 4600

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602

This theorem is referenced by:  elpwid  4609  elelpwi  4610  elpwunsn  4684  elpw2g  5333  f1opw2  7688  eldifpw  7788  pwuncl  7790  iunpw  7791  mptcnfimad  8011  pwssfi  9217  f1opwfi  9396  fi0  9460  marypha1lem  9473  marypha1  9474  marypha2  9479  brwdom2  9613  brwdom3  9622  r1pwss  9824  rankpwi  9863  acndom  10091  acnnum  10092  dfac12r  10187  ackbij2lem1  10258  ackbij1lem6  10264  ackbij1b  10278  isfin2-2  10359  ssfin2  10360  enfin2i  10361  compsscnvlem  10410  compssiso  10414  fin11a  10423  enfin1ai  10424  fin12  10453  fin1a2s  10454  fin1a2  10455  hsmexlem2  10467  tskwe2  10813  inttsk  10814  inatsk  10818  hashbclem  14491  pr2pwpr  14518  elss2prb  14527  qshash  15863  incexclem  15872  incexc  15873  incexc2  15874  rpnnen2lem12  16261  smupf  16515  ramval  17046  ramlb  17057  mrcflem  17649  isacs2  17696  mreacs  17701  acsfn  17702  acsfn1  17704  acsfn2  17706  sscpwex  17859  isacs3lem  18587  isacs4lem  18589  isacs5lem  18590  isacs5  18593  pmtrfrn  19476  oppglsm  19660  acsfn1p  20800  lspf  20972  pptbas  23015  clsf  23056  mretopd  23100  neiptopuni  23138  cncls2  23281  cncls  23282  cnntr  23283  restcnrm  23370  cncmp  23400  tgcmp  23409  uncmp  23411  sscmp  23413  hauscmplem  23414  cmpfi  23416  1stcrest  23461  dis2ndc  23468  lly1stc  23504  dislly  23505  comppfsc  23540  kgentopon  23546  kgen2ss  23563  kgencn  23564  kgencn2  23565  kgencn3  23566  txcmplem2  23650  txcmp  23651  tx1stc  23658  txkgen  23660  xkopt  23663  xkococnlem  23667  xkococn  23668  kqnrmlem1  23751  kqnrmlem2  23752  hmphdis  23804  isfil2  23864  isfild  23866  fbasfip  23876  neifil  23888  trfil2  23895  trufil  23918  fixufil  23930  cfinufil  23936  fin1aufil  23940  fclscmp  24038  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem5  24064  tgpconncompeqg  24120  imasf1oxms  24502  met2ndc  24536  zdis  24838  icccmp  24847  ovolf  25517  ismbl2  25562  cmmbl  25569  nulmbl  25570  nulmbl2  25571  unmbl  25572  shftmbl  25573  voliunlem2  25586  ioombl1  25597  uniioombl  25624  sqff1o  27225  musum  27234  nulsslt  27842  nulssgt  27843  madessno  27899  oldssno  27900  newssno  27901  madebdayim  27926  eengtrkg  29001  edgssv2  29215  upgrreslem  29321  umgrreslem  29322  umgrres1lem  29327  upgrres1  29330  uhgrvd00  29552  rabfodom  32524  elpwincl1  32544  fpwrelmap  32744  cmpcref  33849  pcmplfinf  33860  zarclsint  33871  zarcls  33873  esumcst  34064  esumfsup  34071  esum2d  34094  dmvlsiga  34130  pwsiga  34131  sigaclci  34133  sigainb  34137  insiga  34138  pwldsys  34158  ldgenpisyslem1  34164  ldgenpisyslem3  34166  measinb  34222  measres  34223  cntmeas  34227  volmeas  34232  ddemeas  34237  dya2iocucvr  34286  sxbrsigalem1  34287  omscl  34297  omsf  34298  omsmon  34300  baselcarsg  34308  difelcarsg  34312  carsgsiga  34324  omsmeas  34325  coinflippv  34486  kur14  35221  connpconn  35240  cvmsi  35270  neibastop1  36360  neibastop2lem  36361  neibastop3  36363  onsucsuccmpi  36444  limsucncmpi  36446  bj-elpwg  37053  bj-0int  37102  bj-ismooredr  37110  lindsdom  37621  ismblfin  37668  cover2  37722  sstotbnd3  37783  heibor1  37817  heibor  37828  pclvalN  39892  pclfinN  39902  pclcmpatN  39903  dochfN  41358  elrfi  42705  cmpfiiin  42708  ismrcd2  42710  isnacs3  42721  aomclem2  43067  islssfg  43082  lmhmfgsplit  43098  lnrfg  43131  dfno2  43441  rfovcnvf1od  44017  dssmapnvod  44033  neik0pk1imk0  44060  isotone2  44062  ntrclsneine0lem  44077  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrclsk4  44085  ntrneix2  44106  ntrneik13  44111  ntrrn  44135  dssmapntrcls  44141  ismnushort  44320  sspwtr  44841  sspwtrALT  44842  sspwtrALT2  44843  pwtrVD  44844  pwtrrVD  44845  sspwimp  44938  sspwimpVD  44939  sspwimpcf  44940  sspwimpcfVD  44941  sspwimpALT  44945  sspwimpALT2  44948  ssnnf1octb  45199  dvdmsscn  45951  dvnmptconst  45956  dvnxpaek  45957  dvnmul  45958  dvnprodlem3  45963  ismbl3  46001  ismbl4  46008  stoweidlem57  46072  pwsal  46330  prsal  46333  intsal  46345  salexct  46349  issalnnd  46360  sge0rnre  46379  sge0tsms  46395  sge0cl  46396  sge0fsum  46402  sge0sup  46406  sge0less  46407  sge0gerp  46410  sge0resplit  46421  sge0split  46424  nnfoctbdj  46471  ismeannd  46482  psmeasure  46486  caragen0  46521  caragenunidm  46523  caragenuncl  46528  caragendifcl  46529  omeiunle  46532  carageniuncl  46538  caragensal  46540  caratheodorylem2  46542  0ome  46544  isomennd  46546  caragenel2d  46547  caragencmpl  46550  ovnf  46578  ovn02  46583  ovnsubaddlem1  46585  ovnsubaddlem2  46586  ovnsubadd  46587  hspmbl  46644  isvonmbl  46653  vonmblss2  46657  ovnsubadd2lem  46660  vonvolmbl  46676  nsssmfmbf  46794  smfresal  46803  smfpimbor1lem2  46814  sprsymrelfv  47481  prpair  47488  grtriprop  47908  lincdifsn  48341  lcosslsp  48355  lindslinindsimp1  48374  lincresunit3lem1  48396  lincresunit3lem2  48397  lincresunit3  48398  isclatd  48872  elpglem1  49230  aacllem  49320