Theorem elpwi 4117

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

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  elpwid  4118  elelpwi  4119  elpwunsn  4171  elpw2g  4754  f1opw2  6786  eldifpw  6868  iunpw  6870  f1opwfi  8153  fi0  8209  fiin  8211  marypha1lem  8222  marypha1  8223  marypha2  8228  brwdom2  8361  brwdom3  8370  r1pwss  8530  rankpwi  8569  acndom  8757  acnnum  8758  dfac12r  8851  ackbij2lem1  8924  ackbij1lem6  8930  ackbij1b  8944  isfin2-2  9024  ssfin2  9025  enfin2i  9026  compsscnvlem  9075  compssiso  9079  fin11a  9088  enfin1ai  9089  fin12  9118  fin1a2s  9119  fin1a2  9120  hsmexlem2  9132  tskwe2  9474  inttsk  9475  inatsk  9479  hashbclem  13093  pr2pwpr  13116  elss2prb  13123  qshash  14398  incexclem  14407  incexc  14408  incexc2  14409  rpnnen2lem12  14793  smupf  15038  ramval  15550  ramlb  15561  mrcflem  16089  isacs2  16137  mreacs  16142  acsfn  16143  acsfn1  16145  acsfn2  16147  sscpwex  16298  fpwipodrs  16987  isacs3lem  16989  isacs4lem  16991  isacs5lem  16992  isacs5  16995  pmtrfrn  17701  oppglsm  17880  lspf  18795  pptbas  20622  clsf  20662  mretopd  20706  neiptopuni  20744  cncls2  20887  cncls  20888  cnntr  20889  restcnrm  20976  cncmp  21005  tgcmp  21014  uncmp  21016  sscmp  21018  hauscmplem  21019  cmpfi  21021  1stcrest  21066  dis2ndc  21073  lly1stc  21109  dislly  21110  comppfsc  21145  kgentopon  21151  kgen2ss  21168  kgencn  21169  kgencn2  21170  kgencn3  21171  txcmplem2  21255  txcmp  21256  tx1stc  21263  txkgen  21265  xkopt  21268  xkococnlem  21272  xkococn  21273  kqnrmlem1  21356  kqnrmlem2  21357  hmphdis  21409  isfil2  21470  isfild  21472  fbasfip  21482  neifil  21494  trfil2  21501  trufil  21524  fixufil  21536  cfinufil  21542  fin1aufil  21546  fclscmp  21644  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem5  21670  tgpconcompeqg  21725  imasf1oxms  22104  met2ndc  22138  zdis  22427  icccmp  22436  ovolf  23057  ismbl2  23102  cmmbl  23109  nulmbl  23110  nulmbl2  23111  unmbl  23112  shftmbl  23113  voliunlem2  23126  ioombl1  23137  uniioombl  23163  sqff1o  24708  musum  24717  eengtrkg  25665  usgrares1  25939  rabfodom  28728  elpwincl1  28741  fpwrelmap  28896  cmpcref  29245  pcmplfinf  29256  esumcst  29452  esumfsup  29459  esum2d  29482  dmvlsiga  29519  pwsiga  29520  sigaclci  29522  sigainb  29526  insiga  29527  pwldsys  29547  ldgenpisyslem1  29553  ldgenpisyslem3  29555  measinb  29611  measres  29612  cntmeas  29616  volmeas  29621  ddemeas  29626  dya2iocucvr  29673  sxbrsigalem1  29674  omscl  29684  omsf  29685  omsmon  29687  baselcarsg  29695  difelcarsg  29699  carsgsiga  29711  omsmeas  29712  coinflippv  29872  kur14  30452  conpcon  30471  cvmsi  30501  neibastop1  31524  neibastop2lem  31525  neibastop3  31527  onsucsuccmpi  31612  limsucncmpi  31614  bj-elpw3  32237  lindsdom  32573  ismblfin  32620  cover2  32678  sstotbnd3  32745  heibor1  32779  heibor  32790  pclvalN  34194  pclfinN  34204  pclcmpatN  34205  dochfN  35663  elrfi  36275  cmpfiiin  36278  ismrcd2  36280  isnacs3  36291  aomclem2  36643  islssfg  36658  lmhmfgsplit  36674  lnrfg  36708  acsfn1p  36788  rfovcnvf1od  37318  dssmapnvod  37334  clsk1indlem3  37361  neik0pk1imk0  37365  isotone1  37366  isotone2  37367  ntrclsneine0lem  37382  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrclsk4  37390  ntrneix2  37411  ntrneik13  37416  ntrrn  37440  dssmapntrcls  37446  sspwtr  38070  sspwtrALT  38071  sspwtrALT2  38080  pwtrVD  38081  pwtrrVD  38082  sspwimp  38176  sspwimpVD  38177  sspwimpcf  38178  sspwimpcfVD  38179  sspwimpALT  38183  sspwimpALT2  38186  pwssfi  38236  elpwinss  38241  ssnnf1octb  38377  dvdmsscn  38826  dvnmptconst  38831  dvnxpaek  38832  dvnmul  38833  dvnprodlem3  38838  ismbl3  38879  ismbl4  38886  stoweidlem57  38950  pwsal  39211  prsal  39214  intsal  39224  salexct  39228  issalnnd  39239  sge0rnre  39257  sge0tsms  39273  sge0cl  39274  sge0fsum  39280  sge0sup  39284  sge0less  39285  sge0gerp  39288  sge0resplit  39299  sge0split  39302  nnfoctbdj  39349  ismeannd  39360  psmeasure  39364  caragen0  39396  caragenunidm  39398  caragenuncl  39403  caragendifcl  39404  omeiunle  39407  carageniuncl  39413  caragensal  39415  caratheodorylem2  39417  0ome  39419  isomennd  39421  caragenel2d  39422  caragencmpl  39425  ovnf  39453  ovn02  39458  ovnsubaddlem1  39460  ovnsubaddlem2  39461  ovnsubadd  39462  hspmbl  39519  isvonmbl  39528  vonmblss2  39532  ovnsubadd2lem  39535  vonvolmbl  39551  nsssmfmbf  39665  smfresal  39673  smfpimbor1lem2  39684  edgassv2  40425  umgrres1lem  40529  upgrres1  40532  uhgrvd00  40750  lincdifsn  42007  lcosslsp  42021  lindslinindsimp1  42040  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064  elpglem1  42253  aacllem  42356