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

Theorem elpwi 4008
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 4007 . 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 1823    C_ wss 3461   ~Pcpw 3999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001
This theorem is referenced by:  elpwid  4009  elelpwi  4010  elpwunsn  4057  elpw2g  4600  f1opw2  6501  eldifpw  6585  iunpw  6587  f1opwfi  7816  fi0  7872  fiin  7874  marypha1lem  7885  marypha1  7886  marypha2  7891  brwdom2  7991  brwdom3  8000  r1pwss  8193  rankpwi  8232  acndom  8423  acnnum  8424  dfac12r  8517  ackbij2lem1  8590  ackbij1lem6  8596  ackbij1b  8610  isfin2-2  8690  ssfin2  8691  enfin2i  8692  compsscnvlem  8741  compssiso  8745  fin11a  8754  enfin1ai  8755  fin12  8784  fin1a2s  8785  fin1a2  8786  hsmexlem2  8798  tskwe2  9140  inttsk  9141  inatsk  9145  hashbclem  12485  pr2pwpr  12504  qshash  13721  incexclem  13730  incexc  13731  incexc2  13732  rpnnen2  14043  smupf  14212  ramval  14610  ramlb  14621  mrcflem  15095  isacs2  15142  mreacs  15147  acsfn  15148  acsfn1  15150  acsfn2  15152  sscpwex  15303  fpwipodrs  15993  isacs3lem  15995  isacs4lem  15997  isacs5lem  15998  isacs5  16001  pmtrfrn  16682  oppglsm  16861  lspf  17815  pptbas  19676  clsf  19716  mretopd  19760  neiptopuni  19798  cncls2  19941  cncls  19942  cnntr  19943  restcnrm  20030  cncmp  20059  tgcmp  20068  uncmp  20070  sscmp  20072  hauscmplem  20073  cmpfi  20075  1stcrest  20120  dis2ndc  20127  lly1stc  20163  dislly  20164  comppfsc  20199  kgentopon  20205  kgen2ss  20222  kgencn  20223  kgencn2  20224  kgencn3  20225  txcmplem2  20309  txcmp  20310  tx1stc  20317  txkgen  20319  xkopt  20322  xkococnlem  20326  xkococn  20327  kqnrmlem1  20410  kqnrmlem2  20411  hmphdis  20463  isfil2  20523  isfild  20525  fbasfip  20535  neifil  20547  trfil2  20554  trufil  20577  fixufil  20589  cfinufil  20595  fin1aufil  20599  fclscmp  20697  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALTlem4  20716  ptcmplem5  20722  tgpconcompeqg  20776  imasf1oxms  21158  met2ndc  21192  zdis  21487  icccmp  21496  ovolf  22059  ismbl2  22104  cmmbl  22111  nulmbl  22112  nulmbl2  22113  unmbl  22114  shftmbl  22115  voliunlem2  22127  ioombl1  22138  uniioombl  22164  sqff1o  23654  musum  23665  eengtrkg  24490  usgrares1  24612  rabfodom  27603  elpwincl1  27620  fpwrelmap  27787  cmpcref  28088  pcmplfinf  28099  esumcst  28292  esumfsup  28299  esum2d  28322  dmvlsiga  28359  pwsiga  28360  sigaclci  28362  sigainb  28366  insiga  28367  measinb  28429  measres  28430  cntmeas  28434  volmeas  28440  ddemeas  28445  dya2iocucvr  28492  sxbrsigalem1  28493  omscl  28503  omsf  28504  oms0  28505  omsmon  28506  baselcarsg  28514  difelcarsg  28518  carsgsiga  28530  omsmeas  28531  coinflippv  28686  kur14  28924  conpcon  28944  cvmsi  28974  onsucsuccmpi  30136  limsucncmpi  30138  ismblfin  30295  neibastop1  30417  neibastop2lem  30418  neibastop3  30420  cover2  30444  sstotbnd3  30512  heibor1  30546  heibor  30557  elrfi  30866  cmpfiiin  30869  ismrcd2  30871  isnacs3  30882  aomclem2  31240  islssfg  31255  lmhmfgsplit  31271  lnrfg  31309  acsfn1p  31389  dvdmsscn  31972  dvnmptconst  31977  dvnxpaek  31978  dvnmul  31979  dvnprodlem3  31984  stoweidlem57  32078  uhgraedgrnv  32721  edgssv2ALT  32773  edgssv2  32774  lincdifsn  33279  lcosslsp  33293  lindslinindsimp1  33312  lincresunit3lem1  33334  lincresunit3lem2  33335  lincresunit3  33336  aacllem  33604  sspwtr  34013  sspwtrALT  34014  sspwtrALT2  34023  pwtrVD  34024  pwtrrVD  34025  sspwimp  34119  sspwimpVD  34120  sspwimpcf  34121  sspwimpcfVD  34122  sspwimpALT  34126  sspwimpALT2  34129  pclvalN  36011  pclfinN  36021  pclcmpatN  36022  dochfN  37480
  Copyright terms: Public domain W3C validator