Theorem elpwi 4556

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-pw 4551

This theorem is referenced by:  elpwid  4558  elelpwi  4559  elpwunsn  4636  elpw2g  5273  f1opw2  7607  eldifpw  7707  pwuncl  7709  iunpw  7710  mptcnfimad  7924  pwssfi  9093  f1opwfi  9247  fi0  9311  marypha1lem  9324  marypha1  9325  marypha2  9330  brwdom2  9466  brwdom3  9475  r1pwss  9684  rankpwi  9723  acndom  9949  acnnum  9950  dfac12r  10045  ackbij2lem1  10116  ackbij1lem6  10122  ackbij1b  10136  isfin2-2  10217  ssfin2  10218  enfin2i  10219  compsscnvlem  10268  compssiso  10272  fin11a  10281  enfin1ai  10282  fin12  10311  fin1a2s  10312  fin1a2  10313  hsmexlem2  10325  tskwe2  10671  inttsk  10672  inatsk  10676  hashbclem  14361  pr2pwpr  14388  elss2prb  14397  qshash  15736  incexclem  15745  incexc  15746  incexc2  15747  rpnnen2lem12  16136  smupf  16391  ramval  16922  ramlb  16933  mrcflem  17514  isacs2  17561  mreacs  17566  acsfn  17567  acsfn1  17569  acsfn2  17571  sscpwex  17724  isacs3lem  18450  isacs4lem  18452  isacs5lem  18453  isacs5  18456  pmtrfrn  19372  oppglsm  19556  acsfn1p  20716  lspf  20909  pptbas  22924  clsf  22964  mretopd  23008  neiptopuni  23046  cncls2  23189  cncls  23190  cnntr  23191  restcnrm  23278  cncmp  23308  tgcmp  23317  uncmp  23319  sscmp  23321  hauscmplem  23322  cmpfi  23324  1stcrest  23369  dis2ndc  23376  lly1stc  23412  dislly  23413  comppfsc  23448  kgentopon  23454  kgen2ss  23471  kgencn  23472  kgencn2  23473  kgencn3  23474  txcmplem2  23558  txcmp  23559  tx1stc  23566  txkgen  23568  xkopt  23571  xkococnlem  23575  xkococn  23576  kqnrmlem1  23659  kqnrmlem2  23660  hmphdis  23712  isfil2  23772  isfild  23774  fbasfip  23784  neifil  23796  trfil2  23803  trufil  23826  fixufil  23838  cfinufil  23844  fin1aufil  23848  fclscmp  23946  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  ptcmplem5  23972  tgpconncompeqg  24028  imasf1oxms  24405  met2ndc  24439  zdis  24733  icccmp  24742  ovolf  25411  ismbl2  25456  cmmbl  25463  nulmbl  25464  nulmbl2  25465  unmbl  25466  shftmbl  25467  voliunlem2  25480  ioombl1  25491  uniioombl  25518  sqff1o  27120  musum  27129  nulsslt  27739  nulssgt  27740  madessno  27802  oldssno  27803  newssno  27804  madebdayim  27834  eengtrkg  28966  edgssv2  29178  upgrreslem  29284  umgrreslem  29285  umgrres1lem  29290  upgrres1  29293  uhgrvd00  29515  rabfodom  32487  elpwincl1  32507  fpwrelmap  32720  esplyfval2  33605  cmpcref  33884  pcmplfinf  33895  zarclsint  33906  zarcls  33908  esumcst  34097  esumfsup  34104  esum2d  34127  dmvlsiga  34163  pwsiga  34164  sigaclci  34166  sigainb  34170  insiga  34171  pwldsys  34191  ldgenpisyslem1  34197  ldgenpisyslem3  34199  measinb  34255  measres  34256  cntmeas  34260  volmeas  34265  ddemeas  34270  dya2iocucvr  34318  sxbrsigalem1  34319  omscl  34329  omsf  34330  omsmon  34332  baselcarsg  34340  difelcarsg  34344  carsgsiga  34356  omsmeas  34357  coinflippv  34518  kur14  35281  connpconn  35300  cvmsi  35330  neibastop1  36424  neibastop2lem  36425  neibastop3  36427  onsucsuccmpi  36508  limsucncmpi  36510  bj-elpwg  37117  bj-0int  37166  bj-ismooredr  37174  lindsdom  37674  ismblfin  37721  cover2  37775  sstotbnd3  37836  heibor1  37870  heibor  37881  pclvalN  40009  pclfinN  40019  pclcmpatN  40020  dochfN  41475  elrfi  42811  cmpfiiin  42814  ismrcd2  42816  isnacs3  42827  aomclem2  43172  islssfg  43187  lmhmfgsplit  43203  lnrfg  43236  dfno2  43545  rfovcnvf1od  44121  dssmapnvod  44137  neik0pk1imk0  44164  isotone2  44166  ntrclsneine0lem  44181  ntrclsiso  44184  ntrclsk2  44185  ntrclskb  44186  ntrclsk3  44187  ntrclsk13  44188  ntrclsk4  44189  ntrneix2  44210  ntrneik13  44215  ntrrn  44239  dssmapntrcls  44245  ismnushort  44418  sspwtr  44937  sspwtrALT  44938  sspwtrALT2  44939  pwtrVD  44940  pwtrrVD  44941  sspwimp  45034  sspwimpVD  45035  sspwimpcf  45036  sspwimpcfVD  45037  sspwimpALT  45041  sspwimpALT2  45044  ssnnf1octb  45315  dvdmsscn  46058  dvnmptconst  46063  dvnxpaek  46064  dvnmul  46065  dvnprodlem3  46070  ismbl3  46108  ismbl4  46115  stoweidlem57  46179  pwsal  46437  prsal  46440  intsal  46452  salexct  46456  issalnnd  46467  sge0rnre  46486  sge0tsms  46502  sge0cl  46503  sge0fsum  46509  sge0sup  46513  sge0less  46514  sge0gerp  46517  sge0resplit  46528  sge0split  46531  nnfoctbdj  46578  ismeannd  46589  psmeasure  46593  caragen0  46628  caragenunidm  46630  caragenuncl  46635  caragendifcl  46636  omeiunle  46639  carageniuncl  46645  caragensal  46647  caratheodorylem2  46649  0ome  46651  isomennd  46653  caragenel2d  46654  caragencmpl  46657  ovnf  46685  ovn02  46690  ovnsubaddlem1  46692  ovnsubaddlem2  46693  ovnsubadd  46694  hspmbl  46751  isvonmbl  46760  vonmblss2  46764  ovnsubadd2lem  46767  vonvolmbl  46783  nsssmfmbf  46901  smfresal  46910  smfpimbor1lem2  46921  sprsymrelfv  47618  prpair  47625  grtriprop  48065  lincdifsn  48549  lcosslsp  48563  lindslinindsimp1  48582  lincresunit3lem1  48604  lincresunit3lem2  48605  lincresunit3  48606  isclatd  49107  elpglem1  49836  aacllem  49926