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

Theorem elpwi 4006
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 4005 . 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 1804    C_ wss 3461   ~Pcpw 3997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475  df-pw 3999
This theorem is referenced by:  elpwid  4007  elelpwi  4008  elpwunsn  4055  elpw2g  4600  f1opw2  6513  eldifpw  6597  iunpw  6599  f1opwfi  7826  fi0  7882  fiin  7884  marypha1lem  7895  marypha1  7896  marypha2  7901  brwdom2  8002  brwdom3  8011  r1pwss  8205  rankpwi  8244  acndom  8435  acnnum  8436  dfac12r  8529  ackbij2lem1  8602  ackbij1lem6  8608  ackbij1b  8622  isfin2-2  8702  ssfin2  8703  enfin2i  8704  compsscnvlem  8753  compssiso  8757  fin11a  8766  enfin1ai  8767  fin12  8796  fin1a2s  8797  fin1a2  8798  hsmexlem2  8810  tskwe2  9154  inttsk  9155  inatsk  9159  hashbclem  12480  pr2pwpr  12499  qshash  13618  incexclem  13627  incexc  13628  incexc2  13629  rpnnen2  13836  smupf  14005  ramval  14403  ramlb  14414  mrcflem  14880  isacs2  14927  mreacs  14932  acsfn  14933  acsfn1  14935  acsfn2  14937  sscpwex  15061  fpwipodrs  15668  isacs3lem  15670  isacs4lem  15672  isacs5lem  15673  isacs5  15676  pmtrfrn  16357  oppglsm  16536  lspf  17494  pptbas  19382  clsf  19422  mretopd  19466  neiptopuni  19504  cncls2  19647  cncls  19648  cnntr  19649  restcnrm  19736  cncmp  19765  tgcmp  19774  uncmp  19776  sscmp  19778  hauscmplem  19779  cmpfi  19781  1stcrest  19827  dis2ndc  19834  lly1stc  19870  dislly  19871  comppfsc  19906  kgentopon  19912  kgen2ss  19929  kgencn  19930  kgencn2  19931  kgencn3  19932  txcmplem2  20016  txcmp  20017  tx1stc  20024  txkgen  20026  xkopt  20029  xkococnlem  20033  xkococn  20034  kqnrmlem1  20117  kqnrmlem2  20118  hmphdis  20170  isfil2  20230  isfild  20232  fbasfip  20242  neifil  20254  trfil2  20261  trufil  20284  fixufil  20296  cfinufil  20302  fin1aufil  20306  fclscmp  20404  alexsubALTlem2  20421  alexsubALTlem3  20422  alexsubALTlem4  20423  ptcmplem5  20429  tgpconcompeqg  20483  imasf1oxms  20865  met2ndc  20899  zdis  21194  icccmp  21203  ovolf  21766  ismbl2  21811  cmmbl  21818  nulmbl  21819  nulmbl2  21820  unmbl  21821  shftmbl  21822  voliunlem2  21834  ioombl1  21845  uniioombl  21871  sqff1o  23328  musum  23339  eengtrkg  24160  usgrares1  24282  rabfodom  27276  fpwrelmap  27428  cmpcref  27726  pcmplfinf  27737  esumcst  27944  esumfsup  27949  dmvlsiga  28002  pwsiga  28003  sigaclci  28005  sigainb  28009  insiga  28010  measinb  28065  measres  28066  cntmeas  28070  volmeas  28076  ddemeas  28081  dya2iocucvr  28128  sxbrsigalem1  28129  coinflippv  28295  kur14  28533  conpcon  28553  cvmsi  28583  onsucsuccmpi  29883  limsucncmpi  29885  ismblfin  30030  neibastop1  30152  neibastop2lem  30153  neibastop3  30155  cover2  30179  sstotbnd3  30247  heibor1  30281  heibor  30292  elrfi  30601  cmpfiiin  30604  ismrcd2  30606  isnacs3  30617  aomclem2  30976  islssfg  30991  lmhmfgsplit  31007  lnrfg  31043  acsfn1p  31124  stoweidlem57  31728  uhgraedgrnv  32187  edgssv2ALT  32239  edgssv2  32240  lincdifsn  32760  lcosslsp  32774  lindslinindsimp1  32793  lincresunit3lem1  32815  lincresunit3lem2  32816  lincresunit3  32817  sspwtr  33352  sspwtrALT  33353  sspwtrALT2  33356  pwtrVD  33357  pwtrrVD  33358  sspwimp  33451  sspwimpVD  33452  sspwimpcf  33453  sspwimpcfVD  33454  sspwimpALT  33458  sspwimpALT2  33461  pclvalN  35354  pclfinN  35364  pclcmpatN  35365  dochfN  36823
  Copyright terms: Public domain W3C validator