MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpwi Structured version   Visualization version   GIF version

Theorem elpwi 4116
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 4115 . 2 (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
21ibi 254 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wss 3539  𝒫 cpw 4107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-pw 4109
This theorem is referenced by:  elpwid  4117  elelpwi  4118  elpwunsn  4170  elpw2g  4748  f1opw2  6763  eldifpw  6845  iunpw  6847  f1opwfi  8130  fi0  8186  fiin  8188  marypha1lem  8199  marypha1  8200  marypha2  8205  brwdom2  8338  brwdom3  8347  r1pwss  8507  rankpwi  8546  acndom  8734  acnnum  8735  dfac12r  8828  ackbij2lem1  8901  ackbij1lem6  8907  ackbij1b  8921  isfin2-2  9001  ssfin2  9002  enfin2i  9003  compsscnvlem  9052  compssiso  9056  fin11a  9065  enfin1ai  9066  fin12  9095  fin1a2s  9096  fin1a2  9097  hsmexlem2  9109  tskwe2  9451  inttsk  9452  inatsk  9456  hashbclem  13047  pr2pwpr  13068  elss2prb  13075  qshash  14346  incexclem  14355  incexc  14356  incexc2  14357  rpnnen2lem12  14741  smupf  14986  ramval  15498  ramlb  15509  mrcflem  16037  isacs2  16085  mreacs  16090  acsfn  16091  acsfn1  16093  acsfn2  16095  sscpwex  16246  fpwipodrs  16935  isacs3lem  16937  isacs4lem  16939  isacs5lem  16940  isacs5  16943  pmtrfrn  17649  oppglsm  17828  lspf  18743  pptbas  20569  clsf  20609  mretopd  20653  neiptopuni  20691  cncls2  20834  cncls  20835  cnntr  20836  restcnrm  20923  cncmp  20952  tgcmp  20961  uncmp  20963  sscmp  20965  hauscmplem  20966  cmpfi  20968  1stcrest  21013  dis2ndc  21020  lly1stc  21056  dislly  21057  comppfsc  21092  kgentopon  21098  kgen2ss  21115  kgencn  21116  kgencn2  21117  kgencn3  21118  txcmplem2  21202  txcmp  21203  tx1stc  21210  txkgen  21212  xkopt  21215  xkococnlem  21219  xkococn  21220  kqnrmlem1  21303  kqnrmlem2  21304  hmphdis  21356  isfil2  21417  isfild  21419  fbasfip  21429  neifil  21441  trfil2  21448  trufil  21471  fixufil  21483  cfinufil  21489  fin1aufil  21493  fclscmp  21591  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALTlem4  21611  ptcmplem5  21617  tgpconcompeqg  21672  imasf1oxms  22051  met2ndc  22085  zdis  22374  icccmp  22383  ovolf  23001  ismbl2  23046  cmmbl  23053  nulmbl  23054  nulmbl2  23055  unmbl  23056  shftmbl  23057  voliunlem2  23070  ioombl1  23081  uniioombl  23107  sqff1o  24652  musum  24661  eengtrkg  25610  usgrares1  25732  rabfodom  28521  elpwincl1  28534  fpwrelmap  28689  cmpcref  29038  pcmplfinf  29049  esumcst  29245  esumfsup  29252  esum2d  29275  dmvlsiga  29312  pwsiga  29313  sigaclci  29315  sigainb  29319  insiga  29320  pwldsys  29340  ldgenpisyslem1  29346  ldgenpisyslem3  29348  measinb  29404  measres  29405  cntmeas  29409  volmeas  29414  ddemeas  29419  dya2iocucvr  29466  sxbrsigalem1  29467  omscl  29477  omsf  29478  omsmon  29480  baselcarsg  29488  difelcarsg  29492  carsgsiga  29504  omsmeas  29505  coinflippv  29665  kur14  30245  conpcon  30264  cvmsi  30294  neibastop1  31317  neibastop2lem  31318  neibastop3  31320  onsucsuccmpi  31405  limsucncmpi  31407  bj-elpw3  32020  lindsdom  32356  ismblfin  32403  cover2  32461  sstotbnd3  32528  heibor1  32562  heibor  32573  pclvalN  33977  pclfinN  33987  pclcmpatN  33988  dochfN  35446  elrfi  36058  cmpfiiin  36061  ismrcd2  36063  isnacs3  36074  aomclem2  36426  islssfg  36441  lmhmfgsplit  36457  lnrfg  36491  acsfn1p  36571  rfovcnvf1od  37101  dssmapnvod  37117  clsk1indlem3  37144  neik0pk1imk0  37148  isotone1  37149  isotone2  37150  ntrclsneine0lem  37165  ntrclsiso  37168  ntrclsk2  37169  ntrclskb  37170  ntrclsk3  37171  ntrclsk13  37172  ntrclsk4  37173  ntrneix2  37194  ntrneik13  37199  ntrrn  37223  dssmapntrcls  37229  sspwtr  37853  sspwtrALT  37854  sspwtrALT2  37863  pwtrVD  37864  pwtrrVD  37865  sspwimp  37959  sspwimpVD  37960  sspwimpcf  37961  sspwimpcfVD  37962  sspwimpALT  37966  sspwimpALT2  37969  pwssfi  38019  elpwinss  38024  ssnnf1octb  38160  dvdmsscn  38609  dvnmptconst  38614  dvnxpaek  38615  dvnmul  38616  dvnprodlem3  38621  ismbl3  38662  ismbl4  38669  stoweidlem57  38733  pwsal  38994  prsal  38997  intsal  39007  salexct  39011  issalnnd  39022  sge0rnre  39040  sge0tsms  39056  sge0cl  39057  sge0fsum  39063  sge0sup  39067  sge0less  39068  sge0gerp  39071  sge0resplit  39082  sge0split  39085  nnfoctbdj  39132  ismeannd  39143  psmeasure  39147  caragen0  39179  caragenunidm  39181  caragenuncl  39186  caragendifcl  39187  omeiunle  39190  carageniuncl  39196  caragensal  39198  caratheodorylem2  39200  0ome  39202  isomennd  39204  caragenel2d  39205  caragencmpl  39208  ovnf  39236  ovn02  39241  ovnsubaddlem1  39243  ovnsubaddlem2  39244  ovnsubadd  39245  hspmbl  39302  isvonmbl  39311  vonmblss2  39315  ovnsubadd2lem  39318  vonvolmbl  39334  nsssmfmbf  39448  smfresal  39456  smfpimbor1lem2  39467  edgassv2  40406  umgrres1lem  40510  upgrres1  40513  uhgrvd00  40731  lincdifsn  41988  lcosslsp  42002  lindslinindsimp1  42021  lincresunit3lem1  42043  lincresunit3lem2  42044  lincresunit3  42045  aacllem  42298
  Copyright terms: Public domain W3C validator