Theorem elpwi 4561

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-pw 4556

This theorem is referenced by:  elpwid  4563  elelpwi  4564  elpwunsn  4642  elpw2g  5288  f1opw2  7647  eldifpw  7747  pwuncl  7749  iunpw  7750  mptcnfimad  7963  pwssfi  9141  f1opwfi  9296  fi0  9363  marypha1lem  9376  marypha1  9377  marypha2  9382  brwdom2  9518  brwdom3  9527  r1pwss  9739  rankpwi  9778  acndom  10004  acnnum  10005  dfac12r  10100  ackbij2lem1  10171  ackbij1lem6  10177  ackbij1b  10191  isfin2-2  10273  ssfin2  10274  enfin2i  10275  compsscnvlem  10324  compssiso  10328  fin11a  10337  enfin1ai  10338  fin12  10367  fin1a2s  10368  fin1a2  10369  hsmexlem2  10381  tskwe2  10728  inttsk  10729  inatsk  10733  indval0  12196  hashbclem  14462  pr2pwpr  14489  elss2prb  14498  qshash  15838  incexclem  15849  incexc  15850  incexc2  15851  rpnnen2lem12  16240  smupf  16495  ramval  17027  ramlb  17038  mrcflem  17621  isacs2  17668  mreacs  17673  acsfn  17674  acsfn1  17676  acsfn2  17678  sscpwex  17831  isacs3lem  18557  isacs4lem  18559  isacs5lem  18560  isacs5  18563  pmtrfrn  19481  oppglsm  19665  acsfn1p  20828  lspf  21021  pptbas  23048  clsf  23088  mretopd  23132  neiptopuni  23170  cncls2  23313  cncls  23314  cnntr  23315  restcnrm  23402  cncmp  23432  tgcmp  23441  uncmp  23443  sscmp  23445  hauscmplem  23446  cmpfi  23448  1stcrest  23493  dis2ndc  23500  lly1stc  23536  dislly  23537  comppfsc  23572  kgentopon  23578  kgen2ss  23595  kgencn  23596  kgencn2  23597  kgencn3  23598  txcmplem2  23682  txcmp  23683  tx1stc  23690  txkgen  23692  xkopt  23695  xkococnlem  23699  xkococn  23700  kqnrmlem1  23783  kqnrmlem2  23784  hmphdis  23836  isfil2  23896  isfild  23898  fbasfip  23908  neifil  23920  trfil2  23927  trufil  23950  fixufil  23962  cfinufil  23968  fin1aufil  23972  fclscmp  24070  alexsubALTlem2  24088  alexsubALTlem3  24089  alexsubALTlem4  24090  ptcmplem5  24096  tgpconncompeqg  24152  imasf1oxms  24529  met2ndc  24563  zdis  24857  icccmp  24866  ovolf  25524  ismbl2  25569  cmmbl  25576  nulmbl  25577  nulmbl2  25578  unmbl  25579  shftmbl  25580  voliunlem2  25593  ioombl1  25604  uniioombl  25631  sqff1o  27223  musum  27232  nulslts  27845  nulsgts  27846  madessno  27910  oldssno  27911  newssno  27912  madebdayim  27958  eengtrkg  29133  edgssv2  29345  upgrreslem  29451  umgrreslem  29452  umgrres1lem  29457  upgrres1  29460  uhgrvd00  29681  rabfodom  32653  elpwincl1  32673  fpwrelmap  32885  esplyfval2  33823  cmpcref  34108  pcmplfinf  34119  zarclsint  34130  zarcls  34132  esumcst  34321  esumfsup  34328  esum2d  34351  dmvlsiga  34387  pwsiga  34388  sigaclci  34390  sigainb  34394  insiga  34395  pwldsys  34415  ldgenpisyslem1  34421  ldgenpisyslem3  34423  measinb  34479  measres  34480  cntmeas  34484  volmeas  34489  ddemeas  34494  dya2iocucvr  34542  sxbrsigalem1  34543  omscl  34553  omsf  34554  omsmon  34556  baselcarsg  34564  difelcarsg  34568  carsgsiga  34580  omsmeas  34581  coinflippv  34742  kur14  35530  connpconn  35549  cvmsi  35579  neibastop1  36683  neibastop2lem  36684  neibastop3  36686  onsucsuccmpi  36767  limsucncmpi  36769  bj-elpwg  37501  bj-0int  37555  bj-ismooredr  37563  lindsdom  38077  ismblfin  38124  cover2  38178  sstotbnd3  38239  heibor1  38273  heibor  38284  pclvalN  40478  pclfinN  40488  pclcmpatN  40489  dochfN  41944  elrfi  43239  cmpfiiin  43242  ismrcd2  43244  isnacs3  43255  aomclem2  43596  islssfg  43611  lmhmfgsplit  43627  lnrfg  43660  dfno2  43968  rfovcnvf1od  44544  dssmapnvod  44560  neik0pk1imk0  44587  isotone2  44589  ntrclsneine0lem  44604  ntrclsiso  44607  ntrclsk2  44608  ntrclskb  44609  ntrclsk3  44610  ntrclsk13  44611  ntrclsk4  44612  ntrneix2  44633  ntrneik13  44638  ntrrn  44662  dssmapntrcls  44668  ismnushort  44841  sspwtr  45360  sspwtrALT  45361  sspwtrALT2  45362  pwtrVD  45363  pwtrrVD  45364  sspwimp  45457  sspwimpVD  45458  sspwimpcf  45459  sspwimpcfVD  45460  sspwimpALT  45464  sspwimpALT2  45467  ssnnf1octb  45736  dvdmsscn  46474  dvnmptconst  46479  dvnxpaek  46480  dvnmul  46481  dvnprodlem3  46486  ismbl3  46524  ismbl4  46531  stoweidlem57  46595  pwsal  46853  prsal  46856  intsal  46868  salexct  46872  issalnnd  46883  sge0rnre  46902  sge0tsms  46918  sge0cl  46919  sge0fsum  46925  sge0sup  46929  sge0less  46930  sge0gerp  46933  sge0resplit  46944  sge0split  46947  nnfoctbdj  46994  ismeannd  47005  psmeasure  47009  caragen0  47044  caragenunidm  47046  caragenuncl  47051  caragendifcl  47052  omeiunle  47055  carageniuncl  47061  caragensal  47063  caratheodorylem2  47065  0ome  47067  isomennd  47069  caragenel2d  47070  caragencmpl  47073  ovnf  47101  ovn02  47106  ovnsubaddlem1  47108  ovnsubaddlem2  47109  ovnsubadd  47110  hspmbl  47167  isvonmbl  47176  vonmblss2  47180  ovnsubadd2lem  47183  vonvolmbl  47199  nsssmfmbf  47317  smfresal  47326  smfpimbor1lem2  47337  sprsymrelfv  48064  prpair  48071  grtriprop  48527  lincdifsn  49010  lcosslsp  49024  lindslinindsimp1  49043  lincresunit3lem1  49065  lincresunit3lem2  49066  lincresunit3  49067  isclatd  49568  elpglem1  50296  aacllem  50386