Theorem elpwi 4570

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-pw 4565

This theorem is referenced by:  elpwid  4572  elelpwi  4573  elpwunsn  4651  elpw2g  5305  f1opw2  7667  eldifpw  7768  pwuncl  7770  iunpw  7771  mptcnfimad  7984  pwssfi  9162  f1opwfi  9314  fi0  9381  marypha1lem  9394  marypha1  9395  marypha2  9400  brwdom2  9536  brwdom3  9545  r1pwss  9757  rankpwi  9796  acndom  10036  acnnum  10037  dfac12r  10131  ackbij2lem1  10202  ackbij1lem6  10208  ackbij1b  10222  isfin2-2  10304  ssfin2  10305  enfin2i  10306  compsscnvlem  10355  compssiso  10359  fin11a  10368  enfin1ai  10369  fin12  10398  fin1a2s  10399  fin1a2  10400  hsmexlem2  10412  tskwe2  10759  inttsk  10760  inatsk  10764  indval0  12223  hashbclem  14491  pr2pwpr  14518  elss2prb  14527  qshash  15881  incexclem  15892  incexc  15893  incexc2  15894  rpnnen2lem12  16282  smupf  16537  ramval  17069  ramlb  17080  mrcflem  17663  isacs2  17710  mreacs  17715  acsfn  17716  acsfn1  17718  acsfn2  17720  sscpwex  17873  isacs3lem  18599  isacs4lem  18601  isacs5lem  18602  isacs5  18605  pmtrfrn  19529  oppglsm  19713  acsfn1p  20883  lspf  21076  pptbas  23146  clsf  23186  mretopd  23230  neiptopuni  23268  cncls2  23411  cncls  23412  cnntr  23413  restcnrm  23500  cncmp  23530  tgcmp  23539  uncmp  23541  sscmp  23543  hauscmplem  23544  cmpfi  23546  1stcrest  23591  dis2ndc  23598  lly1stc  23634  dislly  23635  comppfsc  23670  kgentopon  23676  kgen2ss  23693  kgencn  23694  kgencn2  23695  kgencn3  23696  txcmplem2  23780  txcmp  23781  tx1stc  23788  txkgen  23790  xkopt  23793  xkococnlem  23797  xkococn  23798  kqnrmlem1  23881  kqnrmlem2  23882  hmphdis  23934  isfil2  23994  isfild  23996  fbasfip  24006  neifil  24018  trfil2  24025  trufil  24048  fixufil  24060  cfinufil  24066  fin1aufil  24070  fclscmp  24168  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  ptcmplem5  24194  tgpconncompeqg  24250  imasf1oxms  24627  met2ndc  24661  zdis  24955  icccmp  24964  ovolf  25622  ismbl2  25667  cmmbl  25674  nulmbl  25675  nulmbl2  25676  unmbl  25677  shftmbl  25678  voliunlem2  25691  ioombl1  25702  uniioombl  25729  sqff1o  27324  musum  27333  nulslts  27946  nulsgts  27947  madessno  28011  oldssno  28012  newssno  28013  madebdayim  28059  eengtrkg  29314  edgssv2  29526  upgrreslem  29632  umgrreslem  29633  umgrres1lem  29638  upgrres1  29641  uhgrvd00  29862  rabfodom  32829  elpwincl1  32849  fpwrelmap  33056  esplyfval2  33933  cmpcref  34218  pcmplfinf  34229  zarclsint  34240  zarcls  34242  esumcst  34431  esumfsup  34438  esum2d  34461  dmvlsiga  34497  pwsiga  34498  sigaclci  34500  sigainb  34504  insiga  34505  pwldsys  34525  ldgenpisyslem1  34531  ldgenpisyslem3  34533  measinb  34589  measres  34590  cntmeas  34594  volmeas  34599  ddemeas  34604  dya2iocucvr  34652  sxbrsigalem1  34653  omscl  34663  omsf  34664  omsmon  34666  baselcarsg  34674  difelcarsg  34678  carsgsiga  34690  omsmeas  34691  coinflippv  34852  kur14  35686  connpconn  35705  cvmsi  35735  neibastop1  36848  neibastop2lem  36849  neibastop3  36851  onsucsuccmpi  36932  limsucncmpi  36934  bj-elpwg  37666  bj-0int  37721  bj-ismooredr  37729  lindsdom  38243  ismblfin  38290  cover2  38344  sstotbnd3  38405  heibor1  38439  heibor  38450  pclvalN  40642  pclfinN  40652  pclcmpatN  40653  dochfN  42108  elrfi  43405  cmpfiiin  43408  ismrcd2  43410  isnacs3  43421  aomclem2  43762  islssfg  43777  lmhmfgsplit  43793  lnrfg  43826  dfno2  44134  rfovcnvf1od  44710  dssmapnvod  44726  neik0pk1imk0  44753  isotone2  44755  ntrclsneine0lem  44770  ntrclsiso  44773  ntrclsk2  44774  ntrclskb  44775  ntrclsk3  44776  ntrclsk13  44777  ntrclsk4  44778  ntrneix2  44799  ntrneik13  44804  ntrrn  44828  dssmapntrcls  44834  ismnushort  44991  sspwtr  45509  sspwtrALT  45510  sspwtrALT2  45511  pwtrVD  45512  pwtrrVD  45513  sspwimp  45606  sspwimpVD  45607  sspwimpcf  45608  sspwimpcfVD  45609  sspwimpALT  45613  sspwimpALT2  45616  ssnnf1octb  45892  dvdmsscn  46630  dvnmptconst  46635  dvnxpaek  46636  dvnmul  46637  dvnprodlem3  46642  ismbl3  46680  ismbl4  46687  stoweidlem57  46751  pwsal  47009  prsal  47012  intsal  47024  salexct  47028  issalnnd  47039  sge0rnre  47058  sge0tsms  47074  sge0cl  47075  sge0fsum  47081  sge0sup  47085  sge0less  47086  sge0gerp  47089  sge0resplit  47100  sge0split  47103  nnfoctbdj  47150  ismeannd  47161  psmeasure  47165  caragen0  47200  caragenunidm  47202  caragenuncl  47207  caragendifcl  47208  omeiunle  47211  carageniuncl  47217  caragensal  47219  caratheodorylem2  47221  0ome  47223  isomennd  47225  caragenel2d  47226  caragencmpl  47229  ovnf  47257  ovn02  47262  ovnsubaddlem1  47264  ovnsubaddlem2  47265  ovnsubadd  47266  hspmbl  47323  isvonmbl  47332  vonmblss2  47336  ovnsubadd2lem  47339  vonvolmbl  47355  nsssmfmbf  47473  smfresal  47482  smfpimbor1lem2  47493  sprsymrelfv  48220  prpair  48227  grtriprop  48683  lincdifsn  49181  lcosslsp  49195  lindslinindsimp1  49214  lincresunit3lem1  49236  lincresunit3lem2  49237  lincresunit3  49238  isclatd  49738  elpglem1  50466  aacllem  50578