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

Theorem elpwi 3994
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 3993 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 244 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    C_ wss 3442   ~Pcpw 3985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-pw 3987
This theorem is referenced by:  elpwid  3995  elelpwi  3996  elpwunsn  4043  elpw2g  4588  f1opw2  6536  eldifpw  6617  iunpw  6619  f1opwfi  7884  fi0  7940  fiin  7942  marypha1lem  7953  marypha1  7954  marypha2  7959  brwdom2  8088  brwdom3  8097  r1pwss  8254  rankpwi  8293  acndom  8480  acnnum  8481  dfac12r  8574  ackbij2lem1  8647  ackbij1lem6  8653  ackbij1b  8667  isfin2-2  8747  ssfin2  8748  enfin2i  8749  compsscnvlem  8798  compssiso  8802  fin11a  8811  enfin1ai  8812  fin12  8841  fin1a2s  8842  fin1a2  8843  hsmexlem2  8855  tskwe2  9197  inttsk  9198  inatsk  9202  hashbclem  12610  pr2pwpr  12629  qshash  13863  incexclem  13872  incexc  13873  incexc2  13874  rpnnen2  14256  smupf  14426  ramval  14923  ramvalOLD  14924  ramlb  14940  mrcflem  15463  isacs2  15510  mreacs  15515  acsfn  15516  acsfn1  15518  acsfn2  15520  sscpwex  15671  fpwipodrs  16361  isacs3lem  16363  isacs4lem  16365  isacs5lem  16366  isacs5  16369  pmtrfrn  17050  oppglsm  17229  lspf  18132  pptbas  19954  clsf  19994  mretopd  20039  neiptopuni  20077  cncls2  20220  cncls  20221  cnntr  20222  restcnrm  20309  cncmp  20338  tgcmp  20347  uncmp  20349  sscmp  20351  hauscmplem  20352  cmpfi  20354  1stcrest  20399  dis2ndc  20406  lly1stc  20442  dislly  20443  comppfsc  20478  kgentopon  20484  kgen2ss  20501  kgencn  20502  kgencn2  20503  kgencn3  20504  txcmplem2  20588  txcmp  20589  tx1stc  20596  txkgen  20598  xkopt  20601  xkococnlem  20605  xkococn  20606  kqnrmlem1  20689  kqnrmlem2  20690  hmphdis  20742  isfil2  20802  isfild  20804  fbasfip  20814  neifil  20826  trfil2  20833  trufil  20856  fixufil  20868  cfinufil  20874  fin1aufil  20878  fclscmp  20976  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  ptcmplem5  21002  tgpconcompeqg  21057  imasf1oxms  21435  met2ndc  21469  zdis  21745  icccmp  21754  ovolf  22313  ismbl2  22358  cmmbl  22365  nulmbl  22366  nulmbl2  22367  unmbl  22368  shftmbl  22369  voliunlem2  22381  ioombl1  22392  uniioombl  22424  sqff1o  23972  musum  23983  eengtrkg  24861  usgrares1  24983  rabfodom  27976  elpwincl1  27992  fpwrelmap  28161  cmpcref  28516  pcmplfinf  28527  esumcst  28723  esumfsup  28730  esum2d  28753  dmvlsiga  28790  pwsiga  28791  sigaclci  28793  sigainb  28797  insiga  28798  pwldsys  28818  ldgenpisyslem1  28824  ldgenpisyslem3  28826  measinb  28882  measres  28883  cntmeas  28887  volmeas  28893  ddemeas  28898  dya2iocucvr  28945  sxbrsigalem1  28946  omscl  28956  omsf  28957  oms0  28958  omsmon  28959  baselcarsg  28967  difelcarsg  28971  carsgsiga  28983  omsmeas  28984  coinflippv  29142  kur14  29727  conpcon  29746  cvmsi  29776  neibastop1  30800  neibastop2lem  30801  neibastop3  30803  onsucsuccmpi  30888  limsucncmpi  30890  ismblfin  31685  cover2  31744  sstotbnd3  31812  heibor1  31846  heibor  31857  pclvalN  33164  pclfinN  33174  pclcmpatN  33175  dochfN  34633  elrfi  35245  cmpfiiin  35248  ismrcd2  35250  isnacs3  35261  aomclem2  35619  islssfg  35634  lmhmfgsplit  35650  lnrfg  35684  acsfn1p  35764  sspwtr  36849  sspwtrALT  36850  sspwtrALT2  36859  pwtrVD  36860  pwtrrVD  36861  sspwimp  36955  sspwimpVD  36956  sspwimpcf  36957  sspwimpcfVD  36958  sspwimpALT  36962  sspwimpALT2  36965  pwssfi  37021  elpwinss  37028  dvdmsscn  37380  dvnmptconst  37385  dvnxpaek  37386  dvnmul  37387  dvnprodlem3  37392  stoweidlem57  37487  pwsal  37723  prsal  37726  intsal  37736  sge0rnre  37740  sge0tsms  37756  sge0cl  37757  sge0fsum  37763  sge0sup  37767  sge0less  37768  sge0gerp  37771  sge0resplit  37782  sge0split  37785  nnfoctbdj  37803  ismeannd  37814  psmeasure  37818  caragen0  37836  caragenunidm  37838  caragenuncl  37843  caragendifcl  37844  omeiunle  37847  carageniuncl  37853  caragensal  37855  caratheodorylem2  37857  uhgraedgrnv  38419  edgssv2ALT  38471  edgssv2  38472  lincdifsn  38977  lcosslsp  38991  lindslinindsimp1  39010  lincresunit3lem1  39032  lincresunit3lem2  39033  lincresunit3  39034  aacllem  39301
  Copyright terms: Public domain W3C validator