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

Theorem elpwi 3807
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi  |-  ( A  e.  ~P B  ->  A  C_  B )

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 3806 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 233 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    C_ wss 3320   ~Pcpw 3799
This theorem is referenced by:  elpwid  3808  elelpwi  3809  elpw2g  4363  eldifpw  4755  elpwunsn  4757  iunpw  4759  f1opw2  6298  f1opwfi  7410  fi0  7425  fiin  7427  marypha1lem  7438  marypha1  7439  marypha2  7444  brwdom2  7541  brwdom3  7550  r1pwss  7710  rankpwi  7749  acndom  7932  acnnum  7933  dfac12r  8026  ackbij2lem1  8099  ackbij1lem6  8105  ackbij1b  8119  isfin2-2  8199  ssfin2  8200  enfin2i  8201  compsscnvlem  8250  compssiso  8254  fin11a  8263  enfin1ai  8264  fin12  8293  fin1a2s  8294  fin1a2  8295  hsmexlem2  8307  tskwe2  8648  inttsk  8649  inatsk  8653  hashbclem  11701  qshash  12606  incexclem  12616  incexc  12617  incexc2  12618  rpnnen2  12825  smupf  12990  ramval  13376  ramlb  13387  mrcflem  13831  isacs2  13878  mreacs  13883  acsfn  13884  acsfn1  13886  acsfn2  13888  sscpwex  14015  fpwipodrs  14590  isacs3lem  14592  isacs4lem  14594  isacs5lem  14595  isacs5  14598  oppglsm  15276  lspf  16050  pptbas  17072  clsf  17112  mretopd  17156  neiptopuni  17194  cncls2  17337  cncls  17338  cnntr  17339  restcnrm  17426  cncmp  17455  tgcmp  17464  uncmp  17466  sscmp  17468  hauscmplem  17469  cmpfi  17471  1stcrest  17516  dis2ndc  17523  lly1stc  17559  dislly  17560  kgentopon  17570  kgen2ss  17587  kgencn  17588  kgencn2  17589  kgencn3  17590  txcmplem2  17674  txcmp  17675  tx1stc  17682  txkgen  17684  xkopt  17687  xkococnlem  17691  xkococn  17692  tgqtop  17744  kqnrmlem1  17775  kqnrmlem2  17776  hmphdis  17828  isfil2  17888  isfild  17890  fbasfip  17900  neifil  17912  trfil2  17919  isufil2  17940  trufil  17942  fixufil  17954  cfinufil  17960  fin1aufil  17964  fclscmp  18062  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  ptcmplem5  18087  tgpconcompeqg  18141  imasf1oxms  18519  met2ndc  18553  zdis  18847  icccmp  18856  ovolf  19378  ismbl2  19423  cmmbl  19429  nulmbl  19430  nulmbl2  19431  unmbl  19432  shftmbl  19433  voliunlem2  19445  ioombl1  19456  uniioombl  19481  sqff1o  20965  musum  20976  usgrares1  21424  esumcst  24455  esumfsup  24460  dmvlsiga  24512  pwsiga  24513  sigaclci  24515  sigainb  24519  insiga  24520  measinb  24575  measres  24576  cntmeas  24580  volmeas  24587  dya2iocucvr  24634  sxbrsigalem1  24635  coinflippv  24741  kur14  24902  conpcon  24922  cvmsi  24952  onsucsuccmpi  26193  limsucncmpi  26195  ismblfin  26247  comppfsc  26387  neibastop1  26388  neibastop2lem  26389  neibastop3  26391  cover2  26415  sstotbnd3  26485  heibor1  26519  heibor  26530  elrfi  26748  cmpfiiin  26751  ismrcd2  26753  isnacs3  26764  aomclem2  27130  islssfg  27145  lmhmfgsplit  27161  lnrfg  27300  pmtrfrn  27377  acsfn1p  27484  stoweidlem57  27782  uhgraedgrnv  28292  sspwtr  28934  sspwtrALT  28935  sspwtrALT2  28936  pwtrVD  28937  pwtrrVD  28938  sspwimp  29030  sspwimpVD  29031  sspwimpcf  29032  sspwimpcfVD  29033  sspwimpALT  29037  sspwimpALT2  29040  pclvalN  30687  pclfinN  30697  pclcmpatN  30698  dochfN  32154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334  df-pw 3801
  Copyright terms: Public domain W3C validator