Theorem elpwi 4610

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  elpwid  4612  elelpwi  4613  elpwunsn  4688  elpw2g  5345  f1opw2  7661  eldifpw  7755  pwuncl  7757  iunpw  7758  f1opwfi  9356  fi0  9415  marypha1lem  9428  marypha1  9429  marypha2  9434  brwdom2  9568  brwdom3  9577  r1pwss  9779  rankpwi  9818  acndom  10046  acnnum  10047  dfac12r  10141  ackbij2lem1  10214  ackbij1lem6  10220  ackbij1b  10234  isfin2-2  10314  ssfin2  10315  enfin2i  10316  compsscnvlem  10365  compssiso  10369  fin11a  10378  enfin1ai  10379  fin12  10408  fin1a2s  10409  fin1a2  10410  hsmexlem2  10422  tskwe2  10768  inttsk  10769  inatsk  10773  hashbclem  14411  pr2pwpr  14440  elss2prb  14448  qshash  15773  incexclem  15782  incexc  15783  incexc2  15784  rpnnen2lem12  16168  smupf  16419  ramval  16941  ramlb  16952  mrcflem  17550  isacs2  17597  mreacs  17602  acsfn  17603  acsfn1  17605  acsfn2  17607  sscpwex  17762  isacs3lem  18495  isacs4lem  18497  isacs5lem  18498  isacs5  18501  pmtrfrn  19326  oppglsm  19510  acsfn1p  20415  lspf  20585  pptbas  22511  clsf  22552  mretopd  22596  neiptopuni  22634  cncls2  22777  cncls  22778  cnntr  22779  restcnrm  22866  cncmp  22896  tgcmp  22905  uncmp  22907  sscmp  22909  hauscmplem  22910  cmpfi  22912  1stcrest  22957  dis2ndc  22964  lly1stc  23000  dislly  23001  comppfsc  23036  kgentopon  23042  kgen2ss  23059  kgencn  23060  kgencn2  23061  kgencn3  23062  txcmplem2  23146  txcmp  23147  tx1stc  23154  txkgen  23156  xkopt  23159  xkococnlem  23163  xkococn  23164  kqnrmlem1  23247  kqnrmlem2  23248  hmphdis  23300  isfil2  23360  isfild  23362  fbasfip  23372  neifil  23384  trfil2  23391  trufil  23414  fixufil  23426  cfinufil  23432  fin1aufil  23436  fclscmp  23534  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  ptcmplem5  23560  tgpconncompeqg  23616  imasf1oxms  23998  met2ndc  24032  zdis  24332  icccmp  24341  ovolf  24999  ismbl2  25044  cmmbl  25051  nulmbl  25052  nulmbl2  25053  unmbl  25054  shftmbl  25055  voliunlem2  25068  ioombl1  25079  uniioombl  25106  sqff1o  26686  musum  26695  nulsslt  27298  nulssgt  27299  madessno  27355  oldssno  27356  newssno  27357  madebdayim  27382  eengtrkg  28244  edgssv2  28455  upgrreslem  28561  umgrreslem  28562  umgrres1lem  28567  upgrres1  28570  uhgrvd00  28791  rabfodom  31743  elpwincl1  31763  fpwrelmap  31958  cmpcref  32830  pcmplfinf  32841  zarclsint  32852  zarcls  32854  esumcst  33061  esumfsup  33068  esum2d  33091  dmvlsiga  33127  pwsiga  33128  sigaclci  33130  sigainb  33134  insiga  33135  pwldsys  33155  ldgenpisyslem1  33161  ldgenpisyslem3  33163  measinb  33219  measres  33220  cntmeas  33224  volmeas  33229  ddemeas  33234  dya2iocucvr  33283  sxbrsigalem1  33284  omscl  33294  omsf  33295  omsmon  33297  baselcarsg  33305  difelcarsg  33309  carsgsiga  33321  omsmeas  33322  coinflippv  33482  kur14  34207  connpconn  34226  cvmsi  34256  neibastop1  35244  neibastop2lem  35245  neibastop3  35247  onsucsuccmpi  35328  limsucncmpi  35330  bj-elpwg  35933  bj-0int  35982  bj-ismooredr  35990  lindsdom  36482  ismblfin  36529  cover2  36583  sstotbnd3  36644  heibor1  36678  heibor  36689  pclvalN  38761  pclfinN  38771  pclcmpatN  38772  dochfN  40227  elrfi  41432  cmpfiiin  41435  ismrcd2  41437  isnacs3  41448  aomclem2  41797  islssfg  41812  lmhmfgsplit  41828  lnrfg  41861  dfno2  42179  rfovcnvf1od  42755  dssmapnvod  42771  neik0pk1imk0  42798  isotone2  42800  ntrclsneine0lem  42815  ntrclsiso  42818  ntrclsk2  42819  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ntrclsk4  42823  ntrneix2  42844  ntrneik13  42849  ntrrn  42873  dssmapntrcls  42879  ismnushort  43060  sspwtr  43582  sspwtrALT  43583  sspwtrALT2  43584  pwtrVD  43585  pwtrrVD  43586  sspwimp  43679  sspwimpVD  43680  sspwimpcf  43681  sspwimpcfVD  43682  sspwimpALT  43686  sspwimpALT2  43689  pwssfi  43732  ssnnf1octb  43893  dvdmsscn  44652  dvnmptconst  44657  dvnxpaek  44658  dvnmul  44659  dvnprodlem3  44664  ismbl3  44702  ismbl4  44709  stoweidlem57  44773  pwsal  45031  prsal  45034  intsal  45046  salexct  45050  issalnnd  45061  sge0rnre  45080  sge0tsms  45096  sge0cl  45097  sge0fsum  45103  sge0sup  45107  sge0less  45108  sge0gerp  45111  sge0resplit  45122  sge0split  45125  nnfoctbdj  45172  ismeannd  45183  psmeasure  45187  caragen0  45222  caragenunidm  45224  caragenuncl  45229  caragendifcl  45230  omeiunle  45233  carageniuncl  45239  caragensal  45241  caratheodorylem2  45243  0ome  45245  isomennd  45247  caragenel2d  45248  caragencmpl  45251  ovnf  45279  ovn02  45284  ovnsubaddlem1  45286  ovnsubaddlem2  45287  ovnsubadd  45288  hspmbl  45345  isvonmbl  45354  vonmblss2  45358  ovnsubadd2lem  45361  vonvolmbl  45377  nsssmfmbf  45495  smfresal  45504  smfpimbor1lem2  45515  sprsymrelfv  46162  prpair  46169  isomuspgrlem2c  46498  lincdifsn  47105  lcosslsp  47119  lindslinindsimp1  47138  lincresunit3lem1  47160  lincresunit3lem2  47161  lincresunit3  47162  isclatd  47608  elpglem1  47756  aacllem  47848