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

Theorem elpw 3973
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 3484 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3969 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3214 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1758   _Vcvv 3076    C_ wss 3435   ~Pcpw 3967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-in 3442  df-ss 3449  df-pw 3969
This theorem is referenced by:  selpw  3974  prsspw  4152  0elpw  4568  snelpwi  4644  snelpw  4645  prelpwi  4646  sspwb  4648  pwssun  4734  xpsspwOLD  5061  knatar  6156  iunpw  6499  ssenen  7594  fissuni  7726  fipreima  7727  fiin  7782  fipwuni  7786  dffi3  7791  marypha1lem  7793  inf3lem6  7949  tz9.12lem3  8106  rankonidlem  8145  r0weon  8289  infpwfien  8342  dfac5lem4  8406  dfac2  8410  dfac12lem2  8423  enfin2i  8600  isfin1-3  8665  itunitc1  8699  hsmexlem4  8708  hsmexlem5  8709  axdc4lem  8734  pwfseqlem1  8935  eltsk2g  9028  ixxssxr  11422  ioof  11503  fzof  11666  hashbclem  12322  incexclem  13416  ramub1lem1  14204  ramub1lem2  14205  prdsplusg  14514  prdsmulr  14515  prdsvsca  14516  submrc  14684  isacs2  14709  isssc  14851  homaf  15016  catcfuccl  15095  catcxpccl  15135  clatl  15404  fpwipodrs  15452  isacs4lem  15456  isacs5lem  15457  dprd2dlem1  16661  ablfac1b  16692  cssval  18231  tgdom  18714  distop  18731  fctop  18739  cctop  18741  ppttop  18742  pptbas  18743  epttop  18744  mretopd  18827  resttopon  18896  dishaus  19117  discmp  19132  cmpsublem  19133  cmpsub  19134  bwthOLD  19145  concompid  19166  2ndcsep  19194  cldllycmp  19230  dislly  19232  iskgen3  19253  kgencn2  19261  txuni2  19269  dfac14  19322  prdstopn  19332  txcmplem1  19345  txcmplem2  19346  hmphdis  19500  fbssfi  19541  trfbas2  19547  uffixsn  19629  hauspwpwf1  19691  alexsubALTlem2  19751  met1stc  20227  restmetu  20293  icccmplem1  20530  icccmplem2  20531  opnmbllem  21213  sqff1o  22652  umgra1  23411  uslgra1  23442  usgraedgrnv  23447  usgrarnedg  23454  usgraedg4  23456  usgrares1  23474  cusgrarn  23518  eupath2  23752  sspval  24272  esumpcvgval  26671  esumcvg  26679  pwsiga  26717  difelsiga  26720  sigainb  26723  measssd  26773  cntnevol  26786  ddemeas  26795  mbfmcnt  26826  br2base  26827  sxbrsigalem0  26829  oms0  26853  probun  26945  coinfliprv  27008  coinflippv  27009  ballotth  27063  cvmcov2  27307  elfuns  28089  altxpsspw  28151  elhf2  28356  opnmbllem0  28574  neibastop1  28727  neibastop2lem  28728  heiborlem1  28857  heiborlem8  28864  elrfi  29177  ismrcd2  29182  istopclsd  29183  mrefg2  29190  isnacs3  29193  dfac11  29562  islssfg2  29571  lnr2i  29619  stoweidlem57  29999  trsspwALT  31869  trsspwALT2  31870  trsspwALT3  31871  pwtrVD  31877  pclfinN  33867  mapd1o  35616
  Copyright terms: Public domain W3C validator