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

Theorem elpw 3991
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 3491 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3987 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3227 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    e. wcel 1870   _Vcvv 3087    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:  selpw  3992  prsspwOLD  4176  0elpw  4594  snelpwi  4667  snelpw  4668  prelpwi  4669  sspwb  4671  pwssun  4760  xpsspw  4968  knatar  6263  iunpw  6619  ssenen  7752  fissuni  7885  fipreima  7886  fiin  7942  fipwuni  7946  dffi3  7951  marypha1lem  7953  inf3lem6  8138  tz9.12lem3  8259  rankonidlem  8298  r0weon  8442  infpwfien  8491  dfac5lem4  8555  dfac2  8559  dfac12lem2  8572  enfin2i  8749  isfin1-3  8814  itunitc1  8848  hsmexlem4  8857  hsmexlem5  8858  axdc4lem  8883  pwfseqlem1  9082  eltsk2g  9175  ixxssxr  11647  ioof  11732  fzof  11915  hashbclem  12610  incexclem  13872  ramub1lem1  14947  ramub1lem2  14948  prdsplusg  15315  prdsmulr  15316  prdsvsca  15317  submrc  15485  isacs2  15510  isssc  15676  homaf  15876  catcfuccl  15955  catcxpccl  16043  clatl  16313  fpwipodrs  16361  isacs4lem  16365  isacs5lem  16366  dprd2dlem1  17609  ablfac1b  17638  cssval  19176  tgdom  19925  distop  19942  fctop  19950  cctop  19952  ppttop  19953  pptbas  19954  epttop  19955  mretopd  20039  resttopon  20108  dishaus  20329  discmp  20344  cmpsublem  20345  cmpsub  20346  concompid  20377  2ndcsep  20405  cldllycmp  20441  dislly  20443  iskgen3  20495  kgencn2  20503  txuni2  20511  dfac14  20564  prdstopn  20574  txcmplem1  20587  txcmplem2  20588  hmphdis  20742  fbssfi  20783  trfbas2  20789  uffixsn  20871  hauspwpwf1  20933  alexsubALTlem2  20994  met1stc  21467  restmetu  21516  icccmplem1  21751  icccmplem2  21752  opnmbllem  22436  sqff1o  23972  umgra1  24899  uslgra1  24945  usgraedgrnv  24950  usgrarnedg  24957  usgraedg4  24960  usgrares1  24983  cusgrarn  25032  eupath2  25553  sspval  26207  foresf1o  27975  cmpcref  28516  esumpcvgval  28738  esumcvg  28746  esum2d  28753  pwsiga  28791  difelsiga  28794  sigainb  28797  inelpisys  28815  pwldsys  28818  rossros  28841  measssd  28876  cntnevol  28889  ddemeas  28898  mbfmcnt  28929  br2base  28930  sxbrsigalem0  28932  oms0  28958  probun  29078  coinfliprv  29141  ballotth  29196  cvmcov2  29786  elfuns  30467  altxpsspw  30529  elhf2  30727  neibastop1  30800  neibastop2lem  30801  opnmbllem0  31680  heiborlem1  31847  heiborlem8  31854  pclfinN  33174  mapd1o  34925  elrfi  35245  ismrcd2  35250  istopclsd  35251  mrefg2  35258  isnacs3  35261  dfac11  35626  islssfg2  35635  lnr2i  35681  trsspwALT  36846  trsspwALT2  36847  trsspwALT3  36848  pwtrVD  36860  stoweidlem57  37487  intsal  37736  sge0resplit  37782  omeiunltfirp  37849  prelpw  38376
  Copyright terms: Public domain W3C validator