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

Theorem elpwi 3874
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 3873 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 241 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3333   ~Pcpw 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347  df-pw 3867
This theorem is referenced by:  elpwid  3875  elelpwi  3876  elpwunsn  3922  elpw2g  4460  f1opw2  6318  eldifpw  6393  iunpw  6395  f1opwfi  7620  fi0  7675  fiin  7677  marypha1lem  7688  marypha1  7689  marypha2  7694  brwdom2  7793  brwdom3  7802  r1pwss  7996  rankpwi  8035  acndom  8226  acnnum  8227  dfac12r  8320  ackbij2lem1  8393  ackbij1lem6  8399  ackbij1b  8413  isfin2-2  8493  ssfin2  8494  enfin2i  8495  compsscnvlem  8544  compssiso  8548  fin11a  8557  enfin1ai  8558  fin12  8587  fin1a2s  8588  fin1a2  8589  hsmexlem2  8601  tskwe2  8945  inttsk  8946  inatsk  8950  pr2pwpr  12188  hashbclem  12210  qshash  13295  incexclem  13304  incexc  13305  incexc2  13306  rpnnen2  13513  smupf  13679  ramval  14074  ramlb  14085  mrcflem  14549  isacs2  14596  mreacs  14601  acsfn  14602  acsfn1  14604  acsfn2  14606  sscpwex  14733  fpwipodrs  15339  isacs3lem  15341  isacs4lem  15343  isacs5lem  15344  isacs5  15347  pmtrfrn  15969  oppglsm  16146  lspf  17060  pptbas  18617  clsf  18657  mretopd  18701  neiptopuni  18739  cncls2  18882  cncls  18883  cnntr  18884  restcnrm  18971  cncmp  19000  tgcmp  19009  uncmp  19011  sscmp  19013  hauscmplem  19014  cmpfi  19016  1stcrest  19062  dis2ndc  19069  lly1stc  19105  dislly  19106  kgentopon  19116  kgen2ss  19133  kgencn  19134  kgencn2  19135  kgencn3  19136  txcmplem2  19220  txcmp  19221  tx1stc  19228  txkgen  19230  xkopt  19233  xkococnlem  19237  xkococn  19238  tgqtop  19290  kqnrmlem1  19321  kqnrmlem2  19322  hmphdis  19374  isfil2  19434  isfild  19436  fbasfip  19446  neifil  19458  trfil2  19465  isufil2  19486  trufil  19488  fixufil  19500  cfinufil  19506  fin1aufil  19510  fclscmp  19608  alexsubALTlem2  19625  alexsubALTlem3  19626  alexsubALTlem4  19627  ptcmplem5  19633  tgpconcompeqg  19687  imasf1oxms  20069  met2ndc  20103  zdis  20398  icccmp  20407  ovolf  20970  ismbl2  21015  cmmbl  21021  nulmbl  21022  nulmbl2  21023  unmbl  21024  shftmbl  21025  voliunlem2  21037  ioombl1  21048  uniioombl  21074  sqff1o  22525  musum  22536  f1otrg  23122  eengtrkg  23236  usgrares1  23328  esumcst  26519  esumfsup  26524  dmvlsiga  26577  pwsiga  26578  sigaclci  26580  sigainb  26584  insiga  26585  measinb  26640  measres  26641  cntmeas  26645  volmeas  26652  ddemeas  26657  dya2iocucvr  26704  sxbrsigalem1  26705  oms0  26715  omsmon  26716  coinflippv  26871  kur14  27109  conpcon  27129  cvmsi  27159  onsucsuccmpi  28294  limsucncmpi  28296  ismblfin  28437  comppfsc  28584  neibastop1  28585  neibastop2lem  28586  neibastop3  28588  cover2  28612  sstotbnd3  28680  heibor1  28714  heibor  28725  elrfi  29035  cmpfiiin  29038  ismrcd2  29040  isnacs3  29051  aomclem2  29413  islssfg  29428  lmhmfgsplit  29444  lnrfg  29480  acsfn1p  29561  stoweidlem57  29857  uhgraedgrnv  30278  lincdifsn  30963  lcosslsp  30977  lindslinindsimp1  30996  lincresunit3lem1  31018  lincresunit3lem2  31019  lincresunit3  31020  sspwtr  31560  sspwtrALT  31561  sspwtrALT2  31564  pwtrVD  31565  pwtrrVD  31566  sspwimp  31659  sspwimpVD  31660  sspwimpcf  31661  sspwimpcfVD  31662  sspwimpALT  31666  sspwimpALT2  31669  pclvalN  33539  pclfinN  33549  pclcmpatN  33550  dochfN  35006
  Copyright terms: Public domain W3C validator