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

Theorem elpw 3769
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
elpw.1  |-  A  e. 
_V
Assertion
Ref Expression
elpw  |-  ( A  e.  ~P B  <->  A  C_  B
)

Proof of Theorem elpw
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elpw.1 . 2  |-  A  e. 
_V
2 sseq1 3333 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3765 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3049 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   _Vcvv 2920    C_ wss 3284   ~Pcpw 3763
This theorem is referenced by:  elpwg  3770  prsspw  3935  pwpr  3975  pwtp  3976  pwv  3978  sspwuni  4140  iinpw  4143  iunpwss  4144  0elpw  4333  pwuni  4359  snelpwi  4373  snelpw  4374  prelpwi  4375  sspwb  4377  ssextss  4381  pwin  4451  pwunss  4452  pwssun  4453  iunpw  4722  ordpwsuc  4758  xpsspw  4949  xpsspwOLD  4950  fabexg  5587  knatar  6043  sorpsscmpl  6496  qsss  6928  mapval2  7006  pmsspw  7011  uniixp  7048  ssenen  7244  fineqvlem  7286  fissuni  7373  fipreima  7374  fival  7379  fiin  7389  fipwuni  7393  dffi3  7398  marypha1lem  7400  hartogslem1  7471  inf3lem6  7548  tz9.12lem3  7675  rankonidlem  7714  tskwe  7797  r0weon  7854  infpwfien  7903  dfac5lem4  7967  dfac2  7971  dfac12lem2  7984  cfval2  8100  enfin2i  8161  compsscnvlem  8210  isfin1-3  8226  fin1a2lem13  8252  itunitc1  8260  hsmexlem4  8269  hsmexlem5  8270  axdc3lem  8290  axdc4lem  8295  fpwwe2lem1  8466  fpwwe2lem11  8475  fpwwe2lem12  8476  fpwwe  8481  canthwe  8486  pwfseqlem1  8493  eltsk2g  8586  axgroth5  8659  axgroth6  8663  wuncn  9005  ixxssxr  10888  ioof  10962  fzof  11096  hashbclem  11660  incexclem  12575  vdwmc  13305  ramub2  13341  ram0  13349  ramub1lem1  13353  ramub1lem2  13354  restsspw  13618  prdsplusg  13640  prdsmulr  13641  prdsvsca  13642  ismred  13786  mremre  13788  submrc  13812  isacs2  13837  mreacs  13842  acsfn  13843  isssc  13979  homaf  14144  catcfuccl  14223  catcxpccl  14263  fpwipodrs  14549  isacs4lem  14553  isacs5lem  14554  submacs  14724  subgacs  14934  nsgacs  14935  sylow2alem2  15211  sylow2a  15212  sylow3lem3  15222  sylow3lem6  15225  dprdres  15545  subgdmdprd  15551  dprd2dlem1  15558  ablfac1b  15587  pgpfac1lem5  15596  subrgmre  15851  subsubrg2  15854  lssintcl  15999  lssmre  16001  lssacs  16002  cssval  16868  cssmre  16879  istopon  16949  tgval2  16980  tgdom  17002  distop  17019  fctop  17027  cctop  17029  ppttop  17030  pptbas  17031  epttop  17032  cldss2  17053  ntreq0  17100  discld  17112  mretopd  17115  toponmre  17116  neisspw  17130  resttopon  17183  restdis  17200  cnntr  17297  isnrm2  17380  dishaus  17404  cmpcovf  17412  fincmp  17414  discmp  17419  cmpsublem  17420  cmpsub  17421  cmpcld  17423  cmpfi  17429  concompid  17451  is1stc2  17462  2ndcdisj  17476  2ndcsep  17479  llyi  17494  nllyi  17495  nlly2i  17496  llynlly  17497  subislly  17501  restnlly  17502  llyrest  17505  llyidm  17508  nllyidm  17509  cldllycmp  17515  dislly  17517  iskgen3  17538  kgencn2  17546  txuni2  17554  ptuni2  17565  dfac14  17607  prdstopn  17617  txcmplem1  17630  txcmplem2  17631  qtoptop2  17688  qtopuni  17691  tgqtop  17701  hmphdis  17785  isfbas2  17824  fbssfi  17826  trfbas2  17832  isfild  17847  elfg  17860  cfinfil  17882  csdfil  17883  supfil  17884  isufil2  17897  filssufilg  17900  uffix  17910  uffixsn  17914  ufildr  17920  fin1aufil  17921  hauspwpwf1  17976  alexsubb  18034  alexsubALTlem1  18035  alexsubALTlem2  18036  alexsubALT  18039  ptcmplem5  18044  cldsubg  18097  ustfn  18188  ustn0  18207  met1stc  18508  restmetu  18574  dscopn  18578  icccmplem1  18810  icccmplem2  18811  opnmbllem  19450  vitali  19462  sqff1o  20922  umgra1  21318  uslgra1  21349  usgraedgrnv  21354  usgrarnedg  21361  usgraedg4  21363  usgrares1  21381  cusgrarn  21425  eupath2  21659  sspval  22179  shex  22671  dfch2  22866  ishashinf  24116  esumpcvgval  24425  esumcvg  24433  sigaex  24449  sigaval  24450  pwsiga  24470  difelsiga  24473  sigainb  24476  insiga  24477  measssd  24526  measdivcst  24536  cntnevol  24539  mbfmcnt  24575  br2base  24576  sxbrsigalem0  24578  probun  24634  coinfliprv  24697  ballotlem2  24703  ballotth  24752  erdszelem7  24840  erdsze2lem2  24847  rellyscon  24895  cvmcov2  24919  dffr5  25328  elfuns  25672  altxpsspw  25730  elhf2  26024  islocfin  26270  neibastop1  26282  neibastop2lem  26283  neibastop3  26285  topmeet  26287  topjoin  26288  neifg  26294  heibor1lem  26412  heiborlem1  26414  heiborlem8  26421  elrfi  26642  ismrcd1  26646  ismrcd2  26647  istopclsd  26648  mrefg2  26655  isnacs3  26658  pw2f1ocnv  27002  dfac11  27032  islssfg2  27041  filnm  27064  lnr2i  27192  hbtlem6  27205  sdrgacs  27381  stoweidlem57  27677  trsspwALT  28644  trsspwALT2  28645  trsspwALT3  28646  pwtrVD  28650  pclfinN  30386  lcdlss  32106  mapd1o  32135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298  df-pw 3765
  Copyright terms: Public domain W3C validator