Theorem elpwi 4560

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  elpwid  4562  elelpwi  4563  elpwunsn  4638  elpw2g  5275  f1opw2  7608  eldifpw  7708  pwuncl  7710  iunpw  7711  mptcnfimad  7928  pwssfi  9101  f1opwfi  9265  fi0  9329  marypha1lem  9342  marypha1  9343  marypha2  9348  brwdom2  9484  brwdom3  9493  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  10686  inttsk  10687  inatsk  10691  hashbclem  14377  pr2pwpr  14404  elss2prb  14413  qshash  15752  incexclem  15761  incexc  15762  incexc2  15763  rpnnen2lem12  16152  smupf  16407  ramval  16938  ramlb  16949  mrcflem  17530  isacs2  17577  mreacs  17582  acsfn  17583  acsfn1  17585  acsfn2  17587  sscpwex  17740  isacs3lem  18466  isacs4lem  18468  isacs5lem  18469  isacs5  18472  pmtrfrn  19355  oppglsm  19539  acsfn1p  20702  lspf  20895  pptbas  22911  clsf  22951  mretopd  22995  neiptopuni  23033  cncls2  23176  cncls  23177  cnntr  23178  restcnrm  23265  cncmp  23295  tgcmp  23304  uncmp  23306  sscmp  23308  hauscmplem  23309  cmpfi  23311  1stcrest  23356  dis2ndc  23363  lly1stc  23399  dislly  23400  comppfsc  23435  kgentopon  23441  kgen2ss  23458  kgencn  23459  kgencn2  23460  kgencn3  23461  txcmplem2  23545  txcmp  23546  tx1stc  23553  txkgen  23555  xkopt  23558  xkococnlem  23562  xkococn  23563  kqnrmlem1  23646  kqnrmlem2  23647  hmphdis  23699  isfil2  23759  isfild  23761  fbasfip  23771  neifil  23783  trfil2  23790  trufil  23813  fixufil  23825  cfinufil  23831  fin1aufil  23835  fclscmp  23933  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  ptcmplem5  23959  tgpconncompeqg  24015  imasf1oxms  24393  met2ndc  24427  zdis  24721  icccmp  24730  ovolf  25399  ismbl2  25444  cmmbl  25451  nulmbl  25452  nulmbl2  25453  unmbl  25454  shftmbl  25455  voliunlem2  25468  ioombl1  25479  uniioombl  25506  sqff1o  27108  musum  27117  nulsslt  27726  nulssgt  27727  madessno  27788  oldssno  27789  newssno  27790  madebdayim  27820  eengtrkg  28949  edgssv2  29161  upgrreslem  29267  umgrreslem  29268  umgrres1lem  29273  upgrres1  29276  uhgrvd00  29498  rabfodom  32467  elpwincl1  32487  fpwrelmap  32689  cmpcref  33816  pcmplfinf  33827  zarclsint  33838  zarcls  33840  esumcst  34029  esumfsup  34036  esum2d  34059  dmvlsiga  34095  pwsiga  34096  sigaclci  34098  sigainb  34102  insiga  34103  pwldsys  34123  ldgenpisyslem1  34129  ldgenpisyslem3  34131  measinb  34187  measres  34188  cntmeas  34192  volmeas  34197  ddemeas  34202  dya2iocucvr  34251  sxbrsigalem1  34252  omscl  34262  omsf  34263  omsmon  34265  baselcarsg  34273  difelcarsg  34277  carsgsiga  34289  omsmeas  34290  coinflippv  34451  kur14  35188  connpconn  35207  cvmsi  35237  neibastop1  36332  neibastop2lem  36333  neibastop3  36335  onsucsuccmpi  36416  limsucncmpi  36418  bj-elpwg  37025  bj-0int  37074  bj-ismooredr  37082  lindsdom  37593  ismblfin  37640  cover2  37694  sstotbnd3  37755  heibor1  37789  heibor  37800  pclvalN  39869  pclfinN  39879  pclcmpatN  39880  dochfN  41335  elrfi  42667  cmpfiiin  42670  ismrcd2  42672  isnacs3  42683  aomclem2  43028  islssfg  43043  lmhmfgsplit  43059  lnrfg  43092  dfno2  43401  rfovcnvf1od  43977  dssmapnvod  43993  neik0pk1imk0  44020  isotone2  44022  ntrclsneine0lem  44037  ntrclsiso  44040  ntrclsk2  44041  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrclsk4  44045  ntrneix2  44066  ntrneik13  44071  ntrrn  44095  dssmapntrcls  44101  ismnushort  44274  sspwtr  44794  sspwtrALT  44795  sspwtrALT2  44796  pwtrVD  44797  pwtrrVD  44798  sspwimp  44891  sspwimpVD  44892  sspwimpcf  44893  sspwimpcfVD  44894  sspwimpALT  44898  sspwimpALT2  44901  ssnnf1octb  45172  dvdmsscn  45918  dvnmptconst  45923  dvnxpaek  45924  dvnmul  45925  dvnprodlem3  45930  ismbl3  45968  ismbl4  45975  stoweidlem57  46039  pwsal  46297  prsal  46300  intsal  46312  salexct  46316  issalnnd  46327  sge0rnre  46346  sge0tsms  46362  sge0cl  46363  sge0fsum  46369  sge0sup  46373  sge0less  46374  sge0gerp  46377  sge0resplit  46388  sge0split  46391  nnfoctbdj  46438  ismeannd  46449  psmeasure  46453  caragen0  46488  caragenunidm  46490  caragenuncl  46495  caragendifcl  46496  omeiunle  46499  carageniuncl  46505  caragensal  46507  caratheodorylem2  46509  0ome  46511  isomennd  46513  caragenel2d  46514  caragencmpl  46517  ovnf  46545  ovn02  46550  ovnsubaddlem1  46552  ovnsubaddlem2  46553  ovnsubadd  46554  hspmbl  46611  isvonmbl  46620  vonmblss2  46624  ovnsubadd2lem  46627  vonvolmbl  46643  nsssmfmbf  46761  smfresal  46770  smfpimbor1lem2  46781  sprsymrelfv  47479  prpair  47486  grtriprop  47926  lincdifsn  48410  lcosslsp  48424  lindslinindsimp1  48443  lincresunit3lem1  48465  lincresunit3lem2  48466  lincresunit3  48467  isclatd  48968  elpglem1  49697  aacllem  49787