Theorem elpwi 4563

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-pw 4558

This theorem is used by:  elpwid  4565  elelpwi  4566  elpwunsn  4641  elpw2g  5294  f1opw2  7676  eldifpw  7782  pwuncl  7784  iunpw  7785  mptcnfimad  7998  pwssfi  9195  f1opwfi  9348  fi0  9415  marypha1lem  9428  marypha1  9429  marypha2  9434  brwdom2  9570  brwdom3  9579  r1pwss  9794  rankpwi  9835  acndom  10133  acnnum  10134  dfac12r  10228  ackbij2lem1  10299  ackbij1lem6  10305  ackbij1b  10319  isfin2-2  10400  ssfin2  10401  enfin2i  10402  compsscnvlem  10451  compssiso  10455  fin11a  10464  enfin1ai  10465  fin12  10494  fin1a2s  10495  fin1a2  10496  hsmexlem2  10508  tskwe2  10861  inttsk  10862  inatsk  10866  indval0  12327  hashbclem  14600  pr2pwpr  14627  elss2prb  14636  qshash  15999  incexclem  16010  incexc  16011  incexc2  16012  rpnnen2lem12  16398  smupf  16653  ramval  17191  ramlb  17202  mrcflem  17785  isacs2  17832  mreacs  17837  acsfn  17838  acsfn1  17840  acsfn2  17842  sscpwex  17995  isacs3lem  18721  isacs4lem  18723  isacs5lem  18724  isacs5  18727  pmtrfrn  19677  oppglsm  19861  acsfn1p  21061  lspf  21254  lindsdom  22161  pptbas  23331  clsf  23371  mretopd  23415  neiptopuni  23453  cncls2  23596  cncls  23597  cnntr  23598  restcnrm  23685  cncmp  23715  tgcmp  23724  uncmp  23726  sscmp  23728  hauscmplem  23729  cmpfi  23731  1stcrest  23776  dis2ndc  23784  lly1stc  23820  dislly  23821  comppfsc  23856  kgentopon  23862  kgen2ss  23879  kgencn  23880  kgencn2  23881  kgencn3  23882  txcmplem2  23966  txcmp  23967  tx1stc  23974  txkgen  23976  xkopt  23979  xkococnlem  23983  xkococn  23984  kqnrmlem1  24067  kqnrmlem2  24068  hmphdis  24120  isfil2  24180  isfild  24182  fbasfip  24192  neifil  24204  trfil2  24211  trufil  24234  fixufil  24246  cfinufil  24252  fin1aufil  24256  fclscmp  24354  alexsubALTlem2  24372  alexsubALTlem3  24373  alexsubALTlem4  24374  ptcmplem5  24380  tgpconncompeqg  24436  imasf1oxms  24813  met2ndc  24847  zdis  25141  icccmp  25150  ovolf  25808  ismbl2  25853  cmmbl  25860  nulmbl  25861  nulmbl2  25862  unmbl  25863  shftmbl  25864  voliunlem2  25877  ioombl1  25888  uniioombl  25915  sqff1o  27514  musum  27523  nulslts  28166  nulsgts  28167  madessno  28231  oldssno  28232  newssno  28233  madebdayim  28279  eengtrkg  29569  edgssv2  29784  upgrreslem  29890  umgrreslem  29891  umgrres1lem  29896  upgrres1  29899  uhgrvd00  30120  rabfodom  33148  elpwincl1  33168  fpwrelmap  33371  esplyfval2  34243  cmpcref  34528  pcmplfinf  34539  zarclsint  34550  zarcls  34552  esumcst  34741  esumfsup  34748  esum2d  34771  dmvlsiga  34807  pwsiga  34808  sigaclci  34810  sigainb  34815  insiga  34816  pwldsys  34836  ldgenpisyslem1  34842  ldgenpisyslem3  34844  measinb  34900  measres  34901  cntmeas  34905  volmeas  34910  ddemeas  34915  dya2iocucvr  34962  sxbrsigalem1  34963  omscl  34973  omsf  34974  omsmon  34976  baselcarsg  34984  difelcarsg  34988  carsgsiga  35000  omsmeas  35001  coinflippv  35162  kur14  36067  connpconn  36086  cvmsi  36116  neibastop1  37239  neibastop2lem  37240  neibastop3  37242  onsucsuccmpi  37323  limsucncmpi  37325  bj-elpwg  38059  bj-0int  38114  bj-ismooredr  38122  ismblfin  38672  cover2  38742  sstotbnd3  38803  heibor1  38837  heibor  38848  pclvalN  41040  pclfinN  41050  pclcmpatN  41051  dochfN  42506  elrfi  43798  cmpfiiin  43801  ismrcd2  43803  isnacs3  43814  aomclem2  44150  islssfg  44165  lmhmfgsplit  44181  lnrfg  44214  dfno2  44522  rfovcnvf1od  45097  dssmapnvod  45113  neik0pk1imk0  45140  isotone2  45142  ntrclsneine0lem  45157  ntrclsiso  45160  ntrclsk2  45161  ntrclskb  45162  ntrclsk3  45163  ntrclsk13  45164  ntrclsk4  45165  ntrneix2  45186  ntrneik13  45191  ntrrn  45215  dssmapntrcls  45221  ismnushort  45378  sspwtr  45896  sspwtrALT  45897  sspwtrALT2  45898  pwtrVD  45899  pwtrrVD  45900  sspwimp  45993  sspwimpVD  45994  sspwimpcf  45995  sspwimpcfVD  45996  sspwimpALT  46000  sspwimpALT2  46003  ssnnf1octb  46302  dvdmsscn  47039  dvnmptconst  47044  dvnxpaek  47045  dvnmul  47046  dvnprodlem3  47051  ismbl3  47089  ismbl4  47096  stoweidlem57  47160  pwsal  47418  prsal  47421  intsal  47433  salexct  47437  issalnnd  47448  sge0rnre  47467  sge0tsms  47483  sge0cl  47484  sge0fsum  47490  sge0sup  47494  sge0less  47495  sge0gerp  47498  sge0resplit  47509  sge0split  47512  nnfoctbdj  47559  ismeannd  47570  psmeasure  47574  caragen0  47609  caragenunidm  47611  caragenuncl  47616  caragendifcl  47617  omeiunle  47620  carageniuncl  47626  caragensal  47628  caratheodorylem2  47630  0ome  47632  isomennd  47634  caragenel2d  47635  caragencmpl  47638  ovnf  47666  ovn02  47671  ovnsubaddlem1  47673  ovnsubaddlem2  47674  ovnsubadd  47675  hspmbl  47732  isvonmbl  47741  vonmblss2  47745  ovnsubadd2lem  47748  vonvolmbl  47764  nsssmfmbf  47882  smfresal  47891  smfpimbor1lem2  47902  sprsymrelfv  48669  prpair  48676  grtriprop  49132  lincdifsn  49629  lcosslsp  49643  lindslinindsimp1  49662  lincresunit3lem1  49684  lincresunit3lem2  49685  lincresunit3  49686  itscnhlinecirc02p  49990  isclatd  50190  elpglem1  50972  aacllem  51107