Theorem elpwi 4574

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3908  𝒫 cpw 4567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-pw 4569

This theorem is used by:  elpwid  4576  elelpwi  4577  elpwunsn  4655  elpw2g  5309  f1opw2  7678  eldifpw  7776  pwuncl  7778  iunpw  7779  mptcnfimad  7992  pwssfi  9171  f1opwfi  9323  fi0  9390  marypha1lem  9403  marypha1  9404  marypha2  9409  brwdom2  9545  brwdom3  9554  r1pwss  9766  rankpwi  9805  acndom  10054  acnnum  10055  dfac12r  10149  ackbij2lem1  10220  ackbij1lem6  10226  ackbij1b  10240  isfin2-2  10321  ssfin2  10322  enfin2i  10323  compsscnvlem  10372  compssiso  10376  fin11a  10385  enfin1ai  10386  fin12  10415  fin1a2s  10416  fin1a2  10417  hsmexlem2  10429  tskwe2  10776  inttsk  10777  inatsk  10781  indval0  12240  hashbclem  14509  pr2pwpr  14536  elss2prb  14545  qshash  15905  incexclem  15916  incexc  15917  incexc2  15918  rpnnen2lem12  16306  smupf  16561  ramval  17093  ramlb  17104  mrcflem  17687  isacs2  17734  mreacs  17739  acsfn  17740  acsfn1  17742  acsfn2  17744  sscpwex  17897  isacs3lem  18623  isacs4lem  18625  isacs5lem  18626  isacs5  18629  pmtrfrn  19559  oppglsm  19743  acsfn1p  20939  lspf  21132  pptbas  23202  clsf  23242  mretopd  23286  neiptopuni  23324  cncls2  23467  cncls  23468  cnntr  23469  restcnrm  23556  cncmp  23586  tgcmp  23595  uncmp  23597  sscmp  23599  hauscmplem  23600  cmpfi  23602  1stcrest  23647  dis2ndc  23654  lly1stc  23690  dislly  23691  comppfsc  23726  kgentopon  23732  kgen2ss  23749  kgencn  23750  kgencn2  23751  kgencn3  23752  txcmplem2  23836  txcmp  23837  tx1stc  23844  txkgen  23846  xkopt  23849  xkococnlem  23853  xkococn  23854  kqnrmlem1  23937  kqnrmlem2  23938  hmphdis  23990  isfil2  24050  isfild  24052  fbasfip  24062  neifil  24074  trfil2  24081  trufil  24104  fixufil  24116  cfinufil  24122  fin1aufil  24126  fclscmp  24224  alexsubALTlem2  24242  alexsubALTlem3  24243  alexsubALTlem4  24244  ptcmplem5  24250  tgpconncompeqg  24306  imasf1oxms  24683  met2ndc  24717  zdis  25011  icccmp  25020  ovolf  25678  ismbl2  25723  cmmbl  25730  nulmbl  25731  nulmbl2  25732  unmbl  25733  shftmbl  25734  voliunlem2  25747  ioombl1  25758  uniioombl  25785  sqff1o  27383  musum  27392  nulslts  28005  nulsgts  28006  madessno  28070  oldssno  28071  newssno  28072  madebdayim  28118  eengtrkg  29373  edgssv2  29585  upgrreslem  29691  umgrreslem  29692  umgrres1lem  29697  upgrres1  29700  uhgrvd00  29921  rabfodom  32888  elpwincl1  32908  fpwrelmap  33115  esplyfval2  33986  cmpcref  34271  pcmplfinf  34282  zarclsint  34293  zarcls  34295  esumcst  34484  esumfsup  34491  esum2d  34514  dmvlsiga  34550  pwsiga  34551  sigaclci  34553  sigainb  34558  insiga  34559  pwldsys  34579  ldgenpisyslem1  34585  ldgenpisyslem3  34587  measinb  34643  measres  34644  cntmeas  34648  volmeas  34653  ddemeas  34658  dya2iocucvr  34706  sxbrsigalem1  34707  omscl  34717  omsf  34718  omsmon  34720  baselcarsg  34728  difelcarsg  34732  carsgsiga  34744  omsmeas  34745  coinflippv  34906  kur14  35729  connpconn  35748  cvmsi  35778  neibastop1  36911  neibastop2lem  36912  neibastop3  36914  onsucsuccmpi  36995  limsucncmpi  36997  bj-elpwg  37729  bj-0int  37784  bj-ismooredr  37792  lindsdom  38306  ismblfin  38353  cover2  38407  sstotbnd3  38468  heibor1  38502  heibor  38513  pclvalN  40705  pclfinN  40715  pclcmpatN  40716  dochfN  42171  elrfi  43466  cmpfiiin  43469  ismrcd2  43471  isnacs3  43482  aomclem2  43823  islssfg  43838  lmhmfgsplit  43854  lnrfg  43887  dfno2  44195  rfovcnvf1od  44771  dssmapnvod  44787  neik0pk1imk0  44814  isotone2  44816  ntrclsneine0lem  44831  ntrclsiso  44834  ntrclsk2  44835  ntrclskb  44836  ntrclsk3  44837  ntrclsk13  44838  ntrclsk4  44839  ntrneix2  44860  ntrneik13  44865  ntrrn  44889  dssmapntrcls  44895  ismnushort  45052  sspwtr  45570  sspwtrALT  45571  sspwtrALT2  45572  pwtrVD  45573  pwtrrVD  45574  sspwimp  45667  sspwimpVD  45668  sspwimpcf  45669  sspwimpcfVD  45670  sspwimpALT  45674  sspwimpALT2  45677  ssnnf1octb  45953  dvdmsscn  46691  dvnmptconst  46696  dvnxpaek  46697  dvnmul  46698  dvnprodlem3  46703  ismbl3  46741  ismbl4  46748  stoweidlem57  46812  pwsal  47070  prsal  47073  intsal  47085  salexct  47089  issalnnd  47100  sge0rnre  47119  sge0tsms  47135  sge0cl  47136  sge0fsum  47142  sge0sup  47146  sge0less  47147  sge0gerp  47150  sge0resplit  47161  sge0split  47164  nnfoctbdj  47211  ismeannd  47222  psmeasure  47226  caragen0  47261  caragenunidm  47263  caragenuncl  47268  caragendifcl  47269  omeiunle  47272  carageniuncl  47278  caragensal  47280  caratheodorylem2  47282  0ome  47284  isomennd  47286  caragenel2d  47287  caragencmpl  47290  ovnf  47318  ovn02  47323  ovnsubaddlem1  47325  ovnsubaddlem2  47326  ovnsubadd  47327  hspmbl  47384  isvonmbl  47393  vonmblss2  47397  ovnsubadd2lem  47400  vonvolmbl  47416  nsssmfmbf  47534  smfresal  47543  smfpimbor1lem2  47554  sprsymrelfv  48284  prpair  48291  grtriprop  48747  lincdifsn  49245  lcosslsp  49259  lindslinindsimp1  49278  lincresunit3lem1  49300  lincresunit3lem2  49301  lincresunit3  49302  isclatd  49802  elpglem1  50530  aacllem  50662