Theorem elpwi 4539

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  elpwid  4541  elelpwi  4542  elpwunsn  4616  elpw2g  5263  f1opw2  7502  eldifpw  7596  pwuncl  7598  iunpw  7599  f1opwfi  9053  fi0  9109  marypha1lem  9122  marypha1  9123  marypha2  9128  brwdom2  9262  brwdom3  9271  r1pwss  9473  rankpwi  9512  acndom  9738  acnnum  9739  dfac12r  9833  ackbij2lem1  9906  ackbij1lem6  9912  ackbij1b  9926  isfin2-2  10006  ssfin2  10007  enfin2i  10008  compsscnvlem  10057  compssiso  10061  fin11a  10070  enfin1ai  10071  fin12  10100  fin1a2s  10101  fin1a2  10102  hsmexlem2  10114  tskwe2  10460  inttsk  10461  inatsk  10465  hashbclem  14092  pr2pwpr  14121  elss2prb  14129  qshash  15467  incexclem  15476  incexc  15477  incexc2  15478  rpnnen2lem12  15862  smupf  16113  ramval  16637  ramlb  16648  mrcflem  17232  isacs2  17279  mreacs  17284  acsfn  17285  acsfn1  17287  acsfn2  17289  sscpwex  17444  isacs3lem  18175  isacs4lem  18177  isacs5lem  18178  isacs5  18181  pmtrfrn  18981  oppglsm  19162  acsfn1p  19982  lspf  20151  pptbas  22066  clsf  22107  mretopd  22151  neiptopuni  22189  cncls2  22332  cncls  22333  cnntr  22334  restcnrm  22421  cncmp  22451  tgcmp  22460  uncmp  22462  sscmp  22464  hauscmplem  22465  cmpfi  22467  1stcrest  22512  dis2ndc  22519  lly1stc  22555  dislly  22556  comppfsc  22591  kgentopon  22597  kgen2ss  22614  kgencn  22615  kgencn2  22616  kgencn3  22617  txcmplem2  22701  txcmp  22702  tx1stc  22709  txkgen  22711  xkopt  22714  xkococnlem  22718  xkococn  22719  kqnrmlem1  22802  kqnrmlem2  22803  hmphdis  22855  isfil2  22915  isfild  22917  fbasfip  22927  neifil  22939  trfil2  22946  trufil  22969  fixufil  22981  cfinufil  22987  fin1aufil  22991  fclscmp  23089  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem5  23115  tgpconncompeqg  23171  imasf1oxms  23551  met2ndc  23585  zdis  23885  icccmp  23894  ovolf  24551  ismbl2  24596  cmmbl  24603  nulmbl  24604  nulmbl2  24605  unmbl  24606  shftmbl  24607  voliunlem2  24620  ioombl1  24631  uniioombl  24658  sqff1o  26236  musum  26245  eengtrkg  27257  edgssv2  27468  upgrreslem  27574  umgrreslem  27575  umgrres1lem  27580  upgrres1  27583  uhgrvd00  27804  rabfodom  30752  elpwincl1  30775  fpwrelmap  30970  cmpcref  31702  pcmplfinf  31713  zarclsint  31724  zarcls  31726  esumcst  31931  esumfsup  31938  esum2d  31961  dmvlsiga  31997  pwsiga  31998  sigaclci  32000  sigainb  32004  insiga  32005  pwldsys  32025  ldgenpisyslem1  32031  ldgenpisyslem3  32033  measinb  32089  measres  32090  cntmeas  32094  volmeas  32099  ddemeas  32104  dya2iocucvr  32151  sxbrsigalem1  32152  omscl  32162  omsf  32163  omsmon  32165  baselcarsg  32173  difelcarsg  32177  carsgsiga  32189  omsmeas  32190  coinflippv  32350  kur14  33078  connpconn  33097  cvmsi  33127  nulsslt  33918  nulssgt  33919  madessno  33971  oldssno  33972  newssno  33973  madebdayim  33997  neibastop1  34475  neibastop2lem  34476  neibastop3  34478  onsucsuccmpi  34559  limsucncmpi  34561  bj-elpwg  35152  bj-0int  35199  bj-ismooredr  35207  lindsdom  35698  ismblfin  35745  cover2  35799  sstotbnd3  35861  heibor1  35895  heibor  35906  pclvalN  37831  pclfinN  37841  pclcmpatN  37842  dochfN  39297  elrfi  40432  cmpfiiin  40435  ismrcd2  40437  isnacs3  40448  aomclem2  40796  islssfg  40811  lmhmfgsplit  40827  lnrfg  40860  rfovcnvf1od  41501  dssmapnvod  41517  neik0pk1imk0  41546  isotone2  41548  ntrclsneine0lem  41563  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrclsk4  41571  ntrneix2  41592  ntrneik13  41597  ntrrn  41621  dssmapntrcls  41627  ismnushort  41808  sspwtr  42330  sspwtrALT  42331  sspwtrALT2  42332  pwtrVD  42333  pwtrrVD  42334  sspwimp  42427  sspwimpVD  42428  sspwimpcf  42429  sspwimpcfVD  42430  sspwimpALT  42434  sspwimpALT2  42437  pwssfi  42482  ssnnf1octb  42622  dvdmsscn  43367  dvnmptconst  43372  dvnxpaek  43373  dvnmul  43374  dvnprodlem3  43379  ismbl3  43417  ismbl4  43424  stoweidlem57  43488  pwsal  43746  prsal  43749  intsal  43759  salexct  43763  issalnnd  43774  sge0rnre  43792  sge0tsms  43808  sge0cl  43809  sge0fsum  43815  sge0sup  43819  sge0less  43820  sge0gerp  43823  sge0resplit  43834  sge0split  43837  nnfoctbdj  43884  ismeannd  43895  psmeasure  43899  caragen0  43934  caragenunidm  43936  caragenuncl  43941  caragendifcl  43942  omeiunle  43945  carageniuncl  43951  caragensal  43953  caratheodorylem2  43955  0ome  43957  isomennd  43959  caragenel2d  43960  caragencmpl  43963  ovnf  43991  ovn02  43996  ovnsubaddlem1  43998  ovnsubaddlem2  43999  ovnsubadd  44000  hspmbl  44057  isvonmbl  44066  vonmblss2  44070  ovnsubadd2lem  44073  vonvolmbl  44089  nsssmfmbf  44201  smfresal  44209  smfpimbor1lem2  44220  sprsymrelfv  44834  prpair  44841  isomuspgrlem2c  45170  lincdifsn  45653  lcosslsp  45667  lindslinindsimp1  45686  lincresunit3lem1  45708  lincresunit3lem2  45709  lincresunit3  45710  isclatd  46157  elpglem1  46302  aacllem  46391