Theorem elpwi 4549

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpwid  4551  elelpwi  4552  elpwunsn  4629  elpw2g  5270  f1opw2  7615  eldifpw  7715  pwuncl  7717  iunpw  7718  mptcnfimad  7932  pwssfi  9104  f1opwfi  9259  fi0  9326  marypha1lem  9339  marypha1  9340  marypha2  9345  brwdom2  9481  brwdom3  9490  r1pwss  9699  rankpwi  9738  acndom  9964  acnnum  9965  dfac12r  10060  ackbij2lem1  10131  ackbij1lem6  10137  ackbij1b  10151  isfin2-2  10232  ssfin2  10233  enfin2i  10234  compsscnvlem  10283  compssiso  10287  fin11a  10296  enfin1ai  10297  fin12  10326  fin1a2s  10327  fin1a2  10328  hsmexlem2  10340  tskwe2  10687  inttsk  10688  inatsk  10692  indval0  12154  hashbclem  14405  pr2pwpr  14432  elss2prb  14441  qshash  15781  incexclem  15792  incexc  15793  incexc2  15794  rpnnen2lem12  16183  smupf  16438  ramval  16970  ramlb  16981  mrcflem  17563  isacs2  17610  mreacs  17615  acsfn  17616  acsfn1  17618  acsfn2  17620  sscpwex  17773  isacs3lem  18499  isacs4lem  18501  isacs5lem  18502  isacs5  18505  pmtrfrn  19424  oppglsm  19608  acsfn1p  20767  lspf  20960  pptbas  22983  clsf  23023  mretopd  23067  neiptopuni  23105  cncls2  23248  cncls  23249  cnntr  23250  restcnrm  23337  cncmp  23367  tgcmp  23376  uncmp  23378  sscmp  23380  hauscmplem  23381  cmpfi  23383  1stcrest  23428  dis2ndc  23435  lly1stc  23471  dislly  23472  comppfsc  23507  kgentopon  23513  kgen2ss  23530  kgencn  23531  kgencn2  23532  kgencn3  23533  txcmplem2  23617  txcmp  23618  tx1stc  23625  txkgen  23627  xkopt  23630  xkococnlem  23634  xkococn  23635  kqnrmlem1  23718  kqnrmlem2  23719  hmphdis  23771  isfil2  23831  isfild  23833  fbasfip  23843  neifil  23855  trfil2  23862  trufil  23885  fixufil  23897  cfinufil  23903  fin1aufil  23907  fclscmp  24005  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  ptcmplem5  24031  tgpconncompeqg  24087  imasf1oxms  24464  met2ndc  24498  zdis  24792  icccmp  24801  ovolf  25459  ismbl2  25504  cmmbl  25511  nulmbl  25512  nulmbl2  25513  unmbl  25514  shftmbl  25515  voliunlem2  25528  ioombl1  25539  uniioombl  25566  sqff1o  27159  musum  27168  nulslts  27781  nulsgts  27782  madessno  27846  oldssno  27847  newssno  27848  madebdayim  27894  eengtrkg  29069  edgssv2  29281  upgrreslem  29387  umgrreslem  29388  umgrres1lem  29393  upgrres1  29396  uhgrvd00  29618  rabfodom  32590  elpwincl1  32610  fpwrelmap  32821  esplyfval2  33724  cmpcref  34010  pcmplfinf  34021  zarclsint  34032  zarcls  34034  esumcst  34223  esumfsup  34230  esum2d  34253  dmvlsiga  34289  pwsiga  34290  sigaclci  34292  sigainb  34296  insiga  34297  pwldsys  34317  ldgenpisyslem1  34323  ldgenpisyslem3  34325  measinb  34381  measres  34382  cntmeas  34386  volmeas  34391  ddemeas  34396  dya2iocucvr  34444  sxbrsigalem1  34445  omscl  34455  omsf  34456  omsmon  34458  baselcarsg  34466  difelcarsg  34470  carsgsiga  34482  omsmeas  34483  coinflippv  34644  kur14  35414  connpconn  35433  cvmsi  35463  neibastop1  36557  neibastop2lem  36558  neibastop3  36560  onsucsuccmpi  36641  limsucncmpi  36643  bj-elpwg  37375  bj-0int  37429  bj-ismooredr  37437  lindsdom  37949  ismblfin  37996  cover2  38050  sstotbnd3  38111  heibor1  38145  heibor  38156  pclvalN  40350  pclfinN  40360  pclcmpatN  40361  dochfN  41816  elrfi  43140  cmpfiiin  43143  ismrcd2  43145  isnacs3  43156  aomclem2  43501  islssfg  43516  lmhmfgsplit  43532  lnrfg  43565  dfno2  43873  rfovcnvf1od  44449  dssmapnvod  44465  neik0pk1imk0  44492  isotone2  44494  ntrclsneine0lem  44509  ntrclsiso  44512  ntrclsk2  44513  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrclsk4  44517  ntrneix2  44538  ntrneik13  44543  ntrrn  44567  dssmapntrcls  44573  ismnushort  44746  sspwtr  45265  sspwtrALT  45266  sspwtrALT2  45267  pwtrVD  45268  pwtrrVD  45269  sspwimp  45362  sspwimpVD  45363  sspwimpcf  45364  sspwimpcfVD  45365  sspwimpALT  45369  sspwimpALT2  45372  ssnnf1octb  45642  dvdmsscn  46382  dvnmptconst  46387  dvnxpaek  46388  dvnmul  46389  dvnprodlem3  46394  ismbl3  46432  ismbl4  46439  stoweidlem57  46503  pwsal  46761  prsal  46764  intsal  46776  salexct  46780  issalnnd  46791  sge0rnre  46810  sge0tsms  46826  sge0cl  46827  sge0fsum  46833  sge0sup  46837  sge0less  46838  sge0gerp  46841  sge0resplit  46852  sge0split  46855  nnfoctbdj  46902  ismeannd  46913  psmeasure  46917  caragen0  46952  caragenunidm  46954  caragenuncl  46959  caragendifcl  46960  omeiunle  46963  carageniuncl  46969  caragensal  46971  caratheodorylem2  46973  0ome  46975  isomennd  46977  caragenel2d  46978  caragencmpl  46981  ovnf  47009  ovn02  47014  ovnsubaddlem1  47016  ovnsubaddlem2  47017  ovnsubadd  47018  hspmbl  47075  isvonmbl  47084  vonmblss2  47088  ovnsubadd2lem  47091  vonvolmbl  47107  nsssmfmbf  47225  smfresal  47234  smfpimbor1lem2  47245  sprsymrelfv  47966  prpair  47973  grtriprop  48429  lincdifsn  48912  lcosslsp  48926  lindslinindsimp1  48945  lincresunit3lem1  48967  lincresunit3lem2  48968  lincresunit3  48969  isclatd  49470  elpglem1  50198  aacllem  50288