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

Theorem elpw 3854
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 3365 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3850 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3098 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1755   _Vcvv 2962    C_ wss 3316   ~Pcpw 3848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850
This theorem is referenced by:  selpw  3855  prsspw  4033  0elpw  4449  snelpwi  4525  snelpw  4526  prelpwi  4527  sspwb  4529  pwssun  4614  xpsspwOLD  4941  knatar  6035  iunpw  6379  ssenen  7473  fissuni  7604  fipreima  7605  fiin  7660  fipwuni  7664  dffi3  7669  marypha1lem  7671  inf3lem6  7827  tz9.12lem3  7984  rankonidlem  8023  r0weon  8167  infpwfien  8220  dfac5lem4  8284  dfac2  8288  dfac12lem2  8301  enfin2i  8478  isfin1-3  8543  itunitc1  8577  hsmexlem4  8586  hsmexlem5  8587  axdc4lem  8612  pwfseqlem1  8813  eltsk2g  8906  ixxssxr  11300  ioof  11375  fzof  11534  hashbclem  12189  incexclem  13282  ramub1lem1  14070  ramub1lem2  14071  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  submrc  14549  isacs2  14574  isssc  14716  homaf  14881  catcfuccl  14960  catcxpccl  15000  clatl  15269  fpwipodrs  15317  isacs4lem  15321  isacs5lem  15322  dprd2dlem1  16514  ablfac1b  16545  cssval  17949  tgdom  18425  distop  18442  fctop  18450  cctop  18452  ppttop  18453  pptbas  18454  epttop  18455  mretopd  18538  resttopon  18607  dishaus  18828  discmp  18843  cmpsublem  18844  cmpsub  18845  bwthOLD  18856  concompid  18877  2ndcsep  18905  cldllycmp  18941  dislly  18943  iskgen3  18964  kgencn2  18972  txuni2  18980  dfac14  19033  prdstopn  19043  txcmplem1  19056  txcmplem2  19057  hmphdis  19211  fbssfi  19252  trfbas2  19258  uffixsn  19340  hauspwpwf1  19402  alexsubALTlem2  19462  met1stc  19938  restmetu  20004  icccmplem1  20241  icccmplem2  20242  opnmbllem  20923  sqff1o  22405  umgra1  23083  uslgra1  23114  usgraedgrnv  23119  usgrarnedg  23126  usgraedg4  23128  usgrares1  23146  cusgrarn  23190  eupath2  23424  sspval  23944  esumpcvgval  26381  esumcvg  26389  pwsiga  26427  difelsiga  26430  sigainb  26433  measssd  26483  cntnevol  26496  ddemeas  26506  mbfmcnt  26537  br2base  26538  sxbrsigalem0  26540  probun  26650  coinfliprv  26713  coinflippv  26714  ballotth  26768  cvmcov2  27012  elfuns  27793  altxpsspw  27855  elhf2  28060  opnmbllem0  28271  neibastop1  28424  neibastop2lem  28425  heiborlem1  28554  heiborlem8  28561  elrfi  28875  ismrcd2  28880  istopclsd  28881  mrefg2  28888  isnacs3  28891  dfac11  29260  islssfg2  29269  lnr2i  29317  stoweidlem57  29698  trsspwALT  31254  trsspwALT2  31255  trsspwALT3  31256  pwtrVD  31262  pclfinN  33117  mapd1o  34866
  Copyright terms: Public domain W3C validator