Theorem elpwi 4548

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-pw 4543

This theorem is referenced by:  elpwid  4550  elelpwi  4551  elpwunsn  4628  elpw2g  5274  f1opw2  7622  eldifpw  7722  pwuncl  7724  iunpw  7725  mptcnfimad  7939  pwssfi  9111  f1opwfi  9266  fi0  9333  marypha1lem  9346  marypha1  9347  marypha2  9352  brwdom2  9488  brwdom3  9497  r1pwss  9708  rankpwi  9747  acndom  9973  acnnum  9974  dfac12r  10069  ackbij2lem1  10140  ackbij1lem6  10146  ackbij1b  10160  isfin2-2  10241  ssfin2  10242  enfin2i  10243  compsscnvlem  10292  compssiso  10296  fin11a  10305  enfin1ai  10306  fin12  10335  fin1a2s  10336  fin1a2  10337  hsmexlem2  10349  tskwe2  10696  inttsk  10697  inatsk  10701  indval0  12163  hashbclem  14414  pr2pwpr  14441  elss2prb  14450  qshash  15790  incexclem  15801  incexc  15802  incexc2  15803  rpnnen2lem12  16192  smupf  16447  ramval  16979  ramlb  16990  mrcflem  17572  isacs2  17619  mreacs  17624  acsfn  17625  acsfn1  17627  acsfn2  17629  sscpwex  17782  isacs3lem  18508  isacs4lem  18510  isacs5lem  18511  isacs5  18514  pmtrfrn  19433  oppglsm  19617  acsfn1p  20776  lspf  20969  pptbas  22973  clsf  23013  mretopd  23057  neiptopuni  23095  cncls2  23238  cncls  23239  cnntr  23240  restcnrm  23327  cncmp  23357  tgcmp  23366  uncmp  23368  sscmp  23370  hauscmplem  23371  cmpfi  23373  1stcrest  23418  dis2ndc  23425  lly1stc  23461  dislly  23462  comppfsc  23497  kgentopon  23503  kgen2ss  23520  kgencn  23521  kgencn2  23522  kgencn3  23523  txcmplem2  23607  txcmp  23608  tx1stc  23615  txkgen  23617  xkopt  23620  xkococnlem  23624  xkococn  23625  kqnrmlem1  23708  kqnrmlem2  23709  hmphdis  23761  isfil2  23821  isfild  23823  fbasfip  23833  neifil  23845  trfil2  23852  trufil  23875  fixufil  23887  cfinufil  23893  fin1aufil  23897  fclscmp  23995  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem5  24021  tgpconncompeqg  24077  imasf1oxms  24454  met2ndc  24488  zdis  24782  icccmp  24791  ovolf  25449  ismbl2  25494  cmmbl  25501  nulmbl  25502  nulmbl2  25503  unmbl  25504  shftmbl  25505  voliunlem2  25518  ioombl1  25529  uniioombl  25556  sqff1o  27145  musum  27154  nulslts  27767  nulsgts  27768  madessno  27832  oldssno  27833  newssno  27834  madebdayim  27880  eengtrkg  29055  edgssv2  29267  upgrreslem  29373  umgrreslem  29374  umgrres1lem  29379  upgrres1  29382  uhgrvd00  29603  rabfodom  32575  elpwincl1  32595  fpwrelmap  32806  esplyfval2  33709  cmpcref  33994  pcmplfinf  34005  zarclsint  34016  zarcls  34018  esumcst  34207  esumfsup  34214  esum2d  34237  dmvlsiga  34273  pwsiga  34274  sigaclci  34276  sigainb  34280  insiga  34281  pwldsys  34301  ldgenpisyslem1  34307  ldgenpisyslem3  34309  measinb  34365  measres  34366  cntmeas  34370  volmeas  34375  ddemeas  34380  dya2iocucvr  34428  sxbrsigalem1  34429  omscl  34439  omsf  34440  omsmon  34442  baselcarsg  34450  difelcarsg  34454  carsgsiga  34466  omsmeas  34467  coinflippv  34628  kur14  35398  connpconn  35417  cvmsi  35447  neibastop1  36541  neibastop2lem  36542  neibastop3  36544  onsucsuccmpi  36625  limsucncmpi  36627  bj-elpwg  37359  bj-0int  37413  bj-ismooredr  37421  lindsdom  37935  ismblfin  37982  cover2  38036  sstotbnd3  38097  heibor1  38131  heibor  38142  pclvalN  40336  pclfinN  40346  pclcmpatN  40347  dochfN  41802  elrfi  43126  cmpfiiin  43129  ismrcd2  43131  isnacs3  43142  aomclem2  43483  islssfg  43498  lmhmfgsplit  43514  lnrfg  43547  dfno2  43855  rfovcnvf1od  44431  dssmapnvod  44447  neik0pk1imk0  44474  isotone2  44476  ntrclsneine0lem  44491  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrclsk4  44499  ntrneix2  44520  ntrneik13  44525  ntrrn  44549  dssmapntrcls  44555  ismnushort  44728  sspwtr  45247  sspwtrALT  45248  sspwtrALT2  45249  pwtrVD  45250  pwtrrVD  45251  sspwimp  45344  sspwimpVD  45345  sspwimpcf  45346  sspwimpcfVD  45347  sspwimpALT  45351  sspwimpALT2  45354  ssnnf1octb  45624  dvdmsscn  46364  dvnmptconst  46369  dvnxpaek  46370  dvnmul  46371  dvnprodlem3  46376  ismbl3  46414  ismbl4  46421  stoweidlem57  46485  pwsal  46743  prsal  46746  intsal  46758  salexct  46762  issalnnd  46773  sge0rnre  46792  sge0tsms  46808  sge0cl  46809  sge0fsum  46815  sge0sup  46819  sge0less  46820  sge0gerp  46823  sge0resplit  46834  sge0split  46837  nnfoctbdj  46884  ismeannd  46895  psmeasure  46899  caragen0  46934  caragenunidm  46936  caragenuncl  46941  caragendifcl  46942  omeiunle  46945  carageniuncl  46951  caragensal  46953  caratheodorylem2  46955  0ome  46957  isomennd  46959  caragenel2d  46960  caragencmpl  46963  ovnf  46991  ovn02  46996  ovnsubaddlem1  46998  ovnsubaddlem2  46999  ovnsubadd  47000  hspmbl  47057  isvonmbl  47066  vonmblss2  47070  ovnsubadd2lem  47073  vonvolmbl  47089  nsssmfmbf  47207  smfresal  47216  smfpimbor1lem2  47227  sprsymrelfv  47954  prpair  47961  grtriprop  48417  lincdifsn  48900  lcosslsp  48914  lindslinindsimp1  48933  lincresunit3lem1  48955  lincresunit3lem2  48956  lincresunit3  48957  isclatd  49458  elpglem1  50186  aacllem  50276