Theorem elpwi 4582

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-pw 4577

This theorem is referenced by:  elpwid  4584  elelpwi  4585  elpwunsn  4660  elpw2g  5303  f1opw2  7660  eldifpw  7760  pwuncl  7762  iunpw  7763  mptcnfimad  7983  pwssfi  9189  f1opwfi  9366  fi0  9430  marypha1lem  9443  marypha1  9444  marypha2  9449  brwdom2  9585  brwdom3  9594  r1pwss  9796  rankpwi  9835  acndom  10063  acnnum  10064  dfac12r  10159  ackbij2lem1  10230  ackbij1lem6  10236  ackbij1b  10250  isfin2-2  10331  ssfin2  10332  enfin2i  10333  compsscnvlem  10382  compssiso  10386  fin11a  10395  enfin1ai  10396  fin12  10425  fin1a2s  10426  fin1a2  10427  hsmexlem2  10439  tskwe2  10785  inttsk  10786  inatsk  10790  hashbclem  14468  pr2pwpr  14495  elss2prb  14504  qshash  15841  incexclem  15850  incexc  15851  incexc2  15852  rpnnen2lem12  16241  smupf  16495  ramval  17026  ramlb  17037  mrcflem  17616  isacs2  17663  mreacs  17668  acsfn  17669  acsfn1  17671  acsfn2  17673  sscpwex  17826  isacs3lem  18550  isacs4lem  18552  isacs5lem  18553  isacs5  18556  pmtrfrn  19437  oppglsm  19621  acsfn1p  20757  lspf  20929  pptbas  22944  clsf  22984  mretopd  23028  neiptopuni  23066  cncls2  23209  cncls  23210  cnntr  23211  restcnrm  23298  cncmp  23328  tgcmp  23337  uncmp  23339  sscmp  23341  hauscmplem  23342  cmpfi  23344  1stcrest  23389  dis2ndc  23396  lly1stc  23432  dislly  23433  comppfsc  23468  kgentopon  23474  kgen2ss  23491  kgencn  23492  kgencn2  23493  kgencn3  23494  txcmplem2  23578  txcmp  23579  tx1stc  23586  txkgen  23588  xkopt  23591  xkococnlem  23595  xkococn  23596  kqnrmlem1  23679  kqnrmlem2  23680  hmphdis  23732  isfil2  23792  isfild  23794  fbasfip  23804  neifil  23816  trfil2  23823  trufil  23846  fixufil  23858  cfinufil  23864  fin1aufil  23868  fclscmp  23966  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem5  23992  tgpconncompeqg  24048  imasf1oxms  24426  met2ndc  24460  zdis  24754  icccmp  24763  ovolf  25433  ismbl2  25478  cmmbl  25485  nulmbl  25486  nulmbl2  25487  unmbl  25488  shftmbl  25489  voliunlem2  25502  ioombl1  25513  uniioombl  25540  sqff1o  27142  musum  27151  nulsslt  27759  nulssgt  27760  madessno  27816  oldssno  27817  newssno  27818  madebdayim  27843  eengtrkg  28911  edgssv2  29123  upgrreslem  29229  umgrreslem  29230  umgrres1lem  29235  upgrres1  29238  uhgrvd00  29460  rabfodom  32432  elpwincl1  32452  fpwrelmap  32656  cmpcref  33827  pcmplfinf  33838  zarclsint  33849  zarcls  33851  esumcst  34040  esumfsup  34047  esum2d  34070  dmvlsiga  34106  pwsiga  34107  sigaclci  34109  sigainb  34113  insiga  34114  pwldsys  34134  ldgenpisyslem1  34140  ldgenpisyslem3  34142  measinb  34198  measres  34199  cntmeas  34203  volmeas  34208  ddemeas  34213  dya2iocucvr  34262  sxbrsigalem1  34263  omscl  34273  omsf  34274  omsmon  34276  baselcarsg  34284  difelcarsg  34288  carsgsiga  34300  omsmeas  34301  coinflippv  34462  kur14  35184  connpconn  35203  cvmsi  35233  neibastop1  36323  neibastop2lem  36324  neibastop3  36326  onsucsuccmpi  36407  limsucncmpi  36409  bj-elpwg  37016  bj-0int  37065  bj-ismooredr  37073  lindsdom  37584  ismblfin  37631  cover2  37685  sstotbnd3  37746  heibor1  37780  heibor  37791  pclvalN  39855  pclfinN  39865  pclcmpatN  39866  dochfN  41321  elrfi  42664  cmpfiiin  42667  ismrcd2  42669  isnacs3  42680  aomclem2  43026  islssfg  43041  lmhmfgsplit  43057  lnrfg  43090  dfno2  43399  rfovcnvf1od  43975  dssmapnvod  43991  neik0pk1imk0  44018  isotone2  44020  ntrclsneine0lem  44035  ntrclsiso  44038  ntrclsk2  44039  ntrclskb  44040  ntrclsk3  44041  ntrclsk13  44042  ntrclsk4  44043  ntrneix2  44064  ntrneik13  44069  ntrrn  44093  dssmapntrcls  44099  ismnushort  44273  sspwtr  44793  sspwtrALT  44794  sspwtrALT2  44795  pwtrVD  44796  pwtrrVD  44797  sspwimp  44890  sspwimpVD  44891  sspwimpcf  44892  sspwimpcfVD  44893  sspwimpALT  44897  sspwimpALT2  44900  ssnnf1octb  45166  dvdmsscn  45913  dvnmptconst  45918  dvnxpaek  45919  dvnmul  45920  dvnprodlem3  45925  ismbl3  45963  ismbl4  45970  stoweidlem57  46034  pwsal  46292  prsal  46295  intsal  46307  salexct  46311  issalnnd  46322  sge0rnre  46341  sge0tsms  46357  sge0cl  46358  sge0fsum  46364  sge0sup  46368  sge0less  46369  sge0gerp  46372  sge0resplit  46383  sge0split  46386  nnfoctbdj  46433  ismeannd  46444  psmeasure  46448  caragen0  46483  caragenunidm  46485  caragenuncl  46490  caragendifcl  46491  omeiunle  46494  carageniuncl  46500  caragensal  46502  caratheodorylem2  46504  0ome  46506  isomennd  46508  caragenel2d  46509  caragencmpl  46512  ovnf  46540  ovn02  46545  ovnsubaddlem1  46547  ovnsubaddlem2  46548  ovnsubadd  46549  hspmbl  46606  isvonmbl  46615  vonmblss2  46619  ovnsubadd2lem  46622  vonvolmbl  46638  nsssmfmbf  46756  smfresal  46765  smfpimbor1lem2  46776  sprsymrelfv  47456  prpair  47463  grtriprop  47901  lincdifsn  48348  lcosslsp  48362  lindslinindsimp1  48381  lincresunit3lem1  48403  lincresunit3lem2  48404  lincresunit3  48405  isclatd  48905  elpglem1  49523  aacllem  49613