Theorem elpwi 4573

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  elpwid  4575  elelpwi  4576  elpwunsn  4651  elpw2g  5291  f1opw2  7647  eldifpw  7747  pwuncl  7749  iunpw  7750  mptcnfimad  7968  pwssfi  9147  f1opwfi  9314  fi0  9378  marypha1lem  9391  marypha1  9392  marypha2  9397  brwdom2  9533  brwdom3  9542  r1pwss  9744  rankpwi  9783  acndom  10011  acnnum  10012  dfac12r  10107  ackbij2lem1  10178  ackbij1lem6  10184  ackbij1b  10198  isfin2-2  10279  ssfin2  10280  enfin2i  10281  compsscnvlem  10330  compssiso  10334  fin11a  10343  enfin1ai  10344  fin12  10373  fin1a2s  10374  fin1a2  10375  hsmexlem2  10387  tskwe2  10733  inttsk  10734  inatsk  10738  hashbclem  14424  pr2pwpr  14451  elss2prb  14460  qshash  15800  incexclem  15809  incexc  15810  incexc2  15811  rpnnen2lem12  16200  smupf  16455  ramval  16986  ramlb  16997  mrcflem  17574  isacs2  17621  mreacs  17626  acsfn  17627  acsfn1  17629  acsfn2  17631  sscpwex  17784  isacs3lem  18508  isacs4lem  18510  isacs5lem  18511  isacs5  18514  pmtrfrn  19395  oppglsm  19579  acsfn1p  20715  lspf  20887  pptbas  22902  clsf  22942  mretopd  22986  neiptopuni  23024  cncls2  23167  cncls  23168  cnntr  23169  restcnrm  23256  cncmp  23286  tgcmp  23295  uncmp  23297  sscmp  23299  hauscmplem  23300  cmpfi  23302  1stcrest  23347  dis2ndc  23354  lly1stc  23390  dislly  23391  comppfsc  23426  kgentopon  23432  kgen2ss  23449  kgencn  23450  kgencn2  23451  kgencn3  23452  txcmplem2  23536  txcmp  23537  tx1stc  23544  txkgen  23546  xkopt  23549  xkococnlem  23553  xkococn  23554  kqnrmlem1  23637  kqnrmlem2  23638  hmphdis  23690  isfil2  23750  isfild  23752  fbasfip  23762  neifil  23774  trfil2  23781  trufil  23804  fixufil  23816  cfinufil  23822  fin1aufil  23826  fclscmp  23924  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem5  23950  tgpconncompeqg  24006  imasf1oxms  24384  met2ndc  24418  zdis  24712  icccmp  24721  ovolf  25390  ismbl2  25435  cmmbl  25442  nulmbl  25443  nulmbl2  25444  unmbl  25445  shftmbl  25446  voliunlem2  25459  ioombl1  25470  uniioombl  25497  sqff1o  27099  musum  27108  nulsslt  27716  nulssgt  27717  madessno  27775  oldssno  27776  newssno  27777  madebdayim  27806  eengtrkg  28920  edgssv2  29132  upgrreslem  29238  umgrreslem  29239  umgrres1lem  29244  upgrres1  29247  uhgrvd00  29469  rabfodom  32441  elpwincl1  32461  fpwrelmap  32663  cmpcref  33847  pcmplfinf  33858  zarclsint  33869  zarcls  33871  esumcst  34060  esumfsup  34067  esum2d  34090  dmvlsiga  34126  pwsiga  34127  sigaclci  34129  sigainb  34133  insiga  34134  pwldsys  34154  ldgenpisyslem1  34160  ldgenpisyslem3  34162  measinb  34218  measres  34219  cntmeas  34223  volmeas  34228  ddemeas  34233  dya2iocucvr  34282  sxbrsigalem1  34283  omscl  34293  omsf  34294  omsmon  34296  baselcarsg  34304  difelcarsg  34308  carsgsiga  34320  omsmeas  34321  coinflippv  34482  kur14  35210  connpconn  35229  cvmsi  35259  neibastop1  36354  neibastop2lem  36355  neibastop3  36357  onsucsuccmpi  36438  limsucncmpi  36440  bj-elpwg  37047  bj-0int  37096  bj-ismooredr  37104  lindsdom  37615  ismblfin  37662  cover2  37716  sstotbnd3  37777  heibor1  37811  heibor  37822  pclvalN  39891  pclfinN  39901  pclcmpatN  39902  dochfN  41357  elrfi  42689  cmpfiiin  42692  ismrcd2  42694  isnacs3  42705  aomclem2  43051  islssfg  43066  lmhmfgsplit  43082  lnrfg  43115  dfno2  43424  rfovcnvf1od  44000  dssmapnvod  44016  neik0pk1imk0  44043  isotone2  44045  ntrclsneine0lem  44060  ntrclsiso  44063  ntrclsk2  44064  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrclsk4  44068  ntrneix2  44089  ntrneik13  44094  ntrrn  44118  dssmapntrcls  44124  ismnushort  44297  sspwtr  44817  sspwtrALT  44818  sspwtrALT2  44819  pwtrVD  44820  pwtrrVD  44821  sspwimp  44914  sspwimpVD  44915  sspwimpcf  44916  sspwimpcfVD  44917  sspwimpALT  44921  sspwimpALT2  44924  ssnnf1octb  45195  dvdmsscn  45941  dvnmptconst  45946  dvnxpaek  45947  dvnmul  45948  dvnprodlem3  45953  ismbl3  45991  ismbl4  45998  stoweidlem57  46062  pwsal  46320  prsal  46323  intsal  46335  salexct  46339  issalnnd  46350  sge0rnre  46369  sge0tsms  46385  sge0cl  46386  sge0fsum  46392  sge0sup  46396  sge0less  46397  sge0gerp  46400  sge0resplit  46411  sge0split  46414  nnfoctbdj  46461  ismeannd  46472  psmeasure  46476  caragen0  46511  caragenunidm  46513  caragenuncl  46518  caragendifcl  46519  omeiunle  46522  carageniuncl  46528  caragensal  46530  caratheodorylem2  46532  0ome  46534  isomennd  46536  caragenel2d  46537  caragencmpl  46540  ovnf  46568  ovn02  46573  ovnsubaddlem1  46575  ovnsubaddlem2  46576  ovnsubadd  46577  hspmbl  46634  isvonmbl  46643  vonmblss2  46647  ovnsubadd2lem  46650  vonvolmbl  46666  nsssmfmbf  46784  smfresal  46793  smfpimbor1lem2  46804  sprsymrelfv  47499  prpair  47506  grtriprop  47944  lincdifsn  48417  lcosslsp  48431  lindslinindsimp1  48450  lincresunit3lem1  48472  lincresunit3lem2  48473  lincresunit3  48474  isclatd  48975  elpglem1  49704  aacllem  49794