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

Theorem elpw 3933
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 3438 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3929 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3174 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1826   _Vcvv 3034    C_ wss 3389   ~Pcpw 3927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403  df-pw 3929
This theorem is referenced by:  selpw  3934  prsspwOLD  4117  0elpw  4534  snelpwi  4607  snelpw  4608  prelpwi  4609  sspwb  4611  pwssun  4700  xpsspw  5029  knatar  6154  iunpw  6513  ssenen  7610  fissuni  7740  fipreima  7741  fiin  7797  fipwuni  7801  dffi3  7806  marypha1lem  7808  inf3lem6  7964  tz9.12lem3  8120  rankonidlem  8159  r0weon  8303  infpwfien  8356  dfac5lem4  8420  dfac2  8424  dfac12lem2  8437  enfin2i  8614  isfin1-3  8679  itunitc1  8713  hsmexlem4  8722  hsmexlem5  8723  axdc4lem  8748  pwfseqlem1  8947  eltsk2g  9040  ixxssxr  11462  ioof  11543  fzof  11719  hashbclem  12405  incexclem  13650  ramub1lem1  14546  ramub1lem2  14547  prdsplusg  14865  prdsmulr  14866  prdsvsca  14867  submrc  15035  isacs2  15060  isssc  15226  homaf  15426  catcfuccl  15505  catcxpccl  15593  clatl  15863  fpwipodrs  15911  isacs4lem  15915  isacs5lem  15916  dprd2dlem1  17203  ablfac1b  17234  cssval  18804  tgdom  19565  distop  19582  fctop  19590  cctop  19592  ppttop  19593  pptbas  19594  epttop  19595  mretopd  19679  resttopon  19748  dishaus  19969  discmp  19984  cmpsublem  19985  cmpsub  19986  concompid  20017  2ndcsep  20045  cldllycmp  20081  dislly  20083  iskgen3  20135  kgencn2  20143  txuni2  20151  dfac14  20204  prdstopn  20214  txcmplem1  20227  txcmplem2  20228  hmphdis  20382  fbssfi  20423  trfbas2  20429  uffixsn  20511  hauspwpwf1  20573  alexsubALTlem2  20633  met1stc  21109  restmetu  21175  icccmplem1  21412  icccmplem2  21413  opnmbllem  22095  sqff1o  23573  umgra1  24447  uslgra1  24493  usgraedgrnv  24498  usgrarnedg  24505  usgraedg4  24508  usgrares1  24531  cusgrarn  24580  eupath2  25101  sspval  25753  foresf1o  27521  cmpcref  28007  esumpcvgval  28226  esumcvg  28234  esum2d  28241  pwsiga  28279  difelsiga  28282  sigainb  28285  measssd  28342  cntnevol  28355  ddemeas  28364  mbfmcnt  28395  br2base  28396  sxbrsigalem0  28398  oms0  28424  probun  28541  coinfliprv  28604  ballotth  28659  cvmcov2  28909  elfuns  29718  altxpsspw  29780  elhf2  29985  opnmbllem0  30215  neibastop1  30343  neibastop2lem  30344  heiborlem1  30473  heiborlem8  30480  elrfi  30792  ismrcd2  30797  istopclsd  30798  mrefg2  30805  isnacs3  30808  dfac11  31174  islssfg2  31183  lnr2i  31233  stoweidlem57  32005  prelpw  32620  trsspwALT  33956  trsspwALT2  33957  trsspwALT3  33958  pwtrVD  33970  pclfinN  36037  mapd1o  37788  psshepw  38283
  Copyright terms: Public domain W3C validator