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 267	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-pw 4558

This theorem is referenced by:  elpwid  4565  elelpwi  4566  elpwunsn  4643  elpw2g  5280  f1opw2  7623  eldifpw  7723  pwuncl  7725  iunpw  7726  mptcnfimad  7940  pwssfi  9113  f1opwfi  9268  fi0  9335  marypha1lem  9348  marypha1  9349  marypha2  9354  brwdom2  9490  brwdom3  9499  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  hashbclem  14387  pr2pwpr  14414  elss2prb  14423  qshash  15762  incexclem  15771  incexc  15772  incexc2  15773  rpnnen2lem12  16162  smupf  16417  ramval  16948  ramlb  16959  mrcflem  17541  isacs2  17588  mreacs  17593  acsfn  17594  acsfn1  17596  acsfn2  17598  sscpwex  17751  isacs3lem  18477  isacs4lem  18479  isacs5lem  18480  isacs5  18483  pmtrfrn  19399  oppglsm  19583  acsfn1p  20744  lspf  20937  pptbas  22964  clsf  23004  mretopd  23048  neiptopuni  23086  cncls2  23229  cncls  23230  cnntr  23231  restcnrm  23318  cncmp  23348  tgcmp  23357  uncmp  23359  sscmp  23361  hauscmplem  23362  cmpfi  23364  1stcrest  23409  dis2ndc  23416  lly1stc  23452  dislly  23453  comppfsc  23488  kgentopon  23494  kgen2ss  23511  kgencn  23512  kgencn2  23513  kgencn3  23514  txcmplem2  23598  txcmp  23599  tx1stc  23606  txkgen  23608  xkopt  23611  xkococnlem  23615  xkococn  23616  kqnrmlem1  23699  kqnrmlem2  23700  hmphdis  23752  isfil2  23812  isfild  23814  fbasfip  23824  neifil  23836  trfil2  23843  trufil  23866  fixufil  23878  cfinufil  23884  fin1aufil  23888  fclscmp  23986  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem5  24012  tgpconncompeqg  24068  imasf1oxms  24445  met2ndc  24479  zdis  24773  icccmp  24782  ovolf  25451  ismbl2  25496  cmmbl  25503  nulmbl  25504  nulmbl2  25505  unmbl  25506  shftmbl  25507  voliunlem2  25520  ioombl1  25531  uniioombl  25558  sqff1o  27160  musum  27169  nulslts  27783  nulsgts  27784  madessno  27848  oldssno  27849  newssno  27850  madebdayim  27896  eengtrkg  29071  edgssv2  29283  upgrreslem  29389  umgrreslem  29390  umgrres1lem  29395  upgrres1  29398  uhgrvd00  29620  rabfodom  32591  elpwincl1  32611  fpwrelmap  32822  esplyfval2  33741  cmpcref  34027  pcmplfinf  34038  zarclsint  34049  zarcls  34051  esumcst  34240  esumfsup  34247  esum2d  34270  dmvlsiga  34306  pwsiga  34307  sigaclci  34309  sigainb  34313  insiga  34314  pwldsys  34334  ldgenpisyslem1  34340  ldgenpisyslem3  34342  measinb  34398  measres  34399  cntmeas  34403  volmeas  34408  ddemeas  34413  dya2iocucvr  34461  sxbrsigalem1  34462  omscl  34472  omsf  34473  omsmon  34475  baselcarsg  34483  difelcarsg  34487  carsgsiga  34499  omsmeas  34500  coinflippv  34661  kur14  35429  connpconn  35448  cvmsi  35478  neibastop1  36572  neibastop2lem  36573  neibastop3  36575  onsucsuccmpi  36656  limsucncmpi  36658  bj-elpwg  37294  bj-0int  37348  bj-ismooredr  37356  lindsdom  37859  ismblfin  37906  cover2  37960  sstotbnd3  38021  heibor1  38055  heibor  38066  pclvalN  40260  pclfinN  40270  pclcmpatN  40271  dochfN  41726  elrfi  43045  cmpfiiin  43048  ismrcd2  43050  isnacs3  43061  aomclem2  43406  islssfg  43421  lmhmfgsplit  43437  lnrfg  43470  dfno2  43778  rfovcnvf1od  44354  dssmapnvod  44370  neik0pk1imk0  44397  isotone2  44399  ntrclsneine0lem  44414  ntrclsiso  44417  ntrclsk2  44418  ntrclskb  44419  ntrclsk3  44420  ntrclsk13  44421  ntrclsk4  44422  ntrneix2  44443  ntrneik13  44448  ntrrn  44472  dssmapntrcls  44478  ismnushort  44651  sspwtr  45170  sspwtrALT  45171  sspwtrALT2  45172  pwtrVD  45173  pwtrrVD  45174  sspwimp  45267  sspwimpVD  45268  sspwimpcf  45269  sspwimpcfVD  45270  sspwimpALT  45274  sspwimpALT2  45277  ssnnf1octb  45547  dvdmsscn  46288  dvnmptconst  46293  dvnxpaek  46294  dvnmul  46295  dvnprodlem3  46300  ismbl3  46338  ismbl4  46345  stoweidlem57  46409  pwsal  46667  prsal  46670  intsal  46682  salexct  46686  issalnnd  46697  sge0rnre  46716  sge0tsms  46732  sge0cl  46733  sge0fsum  46739  sge0sup  46743  sge0less  46744  sge0gerp  46747  sge0resplit  46758  sge0split  46761  nnfoctbdj  46808  ismeannd  46819  psmeasure  46823  caragen0  46858  caragenunidm  46860  caragenuncl  46865  caragendifcl  46866  omeiunle  46869  carageniuncl  46875  caragensal  46877  caratheodorylem2  46879  0ome  46881  isomennd  46883  caragenel2d  46884  caragencmpl  46887  ovnf  46915  ovn02  46920  ovnsubaddlem1  46922  ovnsubaddlem2  46923  ovnsubadd  46924  hspmbl  46981  isvonmbl  46990  vonmblss2  46994  ovnsubadd2lem  46997  vonvolmbl  47013  nsssmfmbf  47131  smfresal  47140  smfpimbor1lem2  47151  sprsymrelfv  47848  prpair  47855  grtriprop  48295  lincdifsn  48778  lcosslsp  48792  lindslinindsimp1  48811  lincresunit3lem1  48833  lincresunit3lem2  48834  lincresunit3  48835  isclatd  49336  elpglem1  50064  aacllem  50154