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

Theorem elpwi 4021
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 4020 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  ~Pcpw 4012
This theorem is referenced by:  elpwid  4022  elelpwi  4023  elpwunsn  4070  elpw2g  4615  f1opw2  6528  eldifpw  6612  iunpw  6614  f1opwfi  7844  fi0  7900  fiin  7902  marypha1lem  7913  marypha1  7914  marypha2  7919  brwdom2  8020  brwdom3  8029  r1pwss  8223  rankpwi  8262  acndom  8453  acnnum  8454  dfac12r  8547  ackbij2lem1  8620  ackbij1lem6  8626  ackbij1b  8640  isfin2-2  8720  ssfin2  8721  enfin2i  8722  compsscnvlem  8771  compssiso  8775  fin11a  8784  enfin1ai  8785  fin12  8814  fin1a2s  8815  fin1a2  8816  hsmexlem2  8828  tskwe2  9172  inttsk  9173  inatsk  9177  hashbclem  12501  pr2pwpr  12520  qshash  13639  incexclem  13648  incexc  13649  incexc2  13650  rpnnen2  13959  smupf  14128  ramval  14526  ramlb  14537  mrcflem  15003  isacs2  15050  mreacs  15055  acsfn  15056  acsfn1  15058  acsfn2  15060  sscpwex  15184  fpwipodrs  15794  isacs3lem  15796  isacs4lem  15798  isacs5lem  15799  isacs5  15802  pmtrfrn  16483  oppglsm  16662  lspf  17620  pptbas  19509  clsf  19549  mretopd  19593  neiptopuni  19631  cncls2  19774  cncls  19775  cnntr  19776  restcnrm  19863  cncmp  19892  tgcmp  19901  uncmp  19903  sscmp  19905  hauscmplem  19906  cmpfi  19908  1stcrest  19954  dis2ndc  19961  lly1stc  19997  dislly  19998  comppfsc  20033  kgentopon  20039  kgen2ss  20056  kgencn  20057  kgencn2  20058  kgencn3  20059  txcmplem2  20143  txcmp  20144  tx1stc  20151  txkgen  20153  xkopt  20156  xkococnlem  20160  xkococn  20161  kqnrmlem1  20244  kqnrmlem2  20245  hmphdis  20297  isfil2  20357  isfild  20359  fbasfip  20369  neifil  20381  trfil2  20388  trufil  20411  fixufil  20423  cfinufil  20429  fin1aufil  20433  fclscmp  20531  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem5  20556  tgpconcompeqg  20610  imasf1oxms  20992  met2ndc  21026  zdis  21321  icccmp  21330  ovolf  21893  ismbl2  21938  cmmbl  21945  nulmbl  21946  nulmbl2  21947  unmbl  21948  shftmbl  21949  voliunlem2  21961  ioombl1  21972  uniioombl  21998  sqff1o  23456  musum  23467  eengtrkg  24288  usgrares1  24410  rabfodom  27404  fpwrelmap  27556  cmpcref  27853  pcmplfinf  27864  esumcst  28071  esumfsup  28076  dmvlsiga  28129  pwsiga  28130  sigaclci  28132  sigainb  28136  insiga  28137  measinb  28192  measres  28193  cntmeas  28197  volmeas  28203  ddemeas  28208  dya2iocucvr  28255  sxbrsigalem1  28256  coinflippv  28422  kur14  28660  conpcon  28680  cvmsi  28710  onsucsuccmpi  29908  limsucncmpi  29910  ismblfin  30055  neibastop1  30177  neibastop2lem  30178  neibastop3  30180  cover2  30204  sstotbnd3  30272  heibor1  30306  heibor  30317  elrfi  30626  cmpfiiin  30629  ismrcd2  30631  isnacs3  30642  aomclem2  31001  islssfg  31016  lmhmfgsplit  31032  lnrfg  31068  acsfn1p  31148  dvdmsscn  31733  dvnmptconst  31738  dvnxpaek  31739  dvnmul  31740  dvnprodlem3  31745  stoweidlem57  31839  uhgraedgrnv  32349  edgssv2ALT  32401  edgssv2  32402  lincdifsn  33025  lcosslsp  33039  lindslinindsimp1  33058  lincresunit3lem1  33080  lincresunit3lem2  33081  lincresunit3  33082  aacllem  33216  sspwtr  33619  sspwtrALT  33620  sspwtrALT2  33623  pwtrVD  33624  pwtrrVD  33625  sspwimp  33718  sspwimpVD  33719  sspwimpcf  33720  sspwimpcfVD  33721  sspwimpALT  33725  sspwimpALT2  33728  pclvalN  35614  pclfinN  35624  pclcmpatN  35625  dochfN  37083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator