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

Theorem elpw 3861
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 3372 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3857 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3104 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1756   _Vcvv 2967    C_ wss 3323   ~Pcpw 3855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857
This theorem is referenced by:  selpw  3862  prsspw  4040  0elpw  4456  snelpwi  4532  snelpw  4533  prelpwi  4534  sspwb  4536  pwssun  4622  xpsspwOLD  4949  knatar  6043  iunpw  6385  ssenen  7477  fissuni  7608  fipreima  7609  fiin  7664  fipwuni  7668  dffi3  7673  marypha1lem  7675  inf3lem6  7831  tz9.12lem3  7988  rankonidlem  8027  r0weon  8171  infpwfien  8224  dfac5lem4  8288  dfac2  8292  dfac12lem2  8305  enfin2i  8482  isfin1-3  8547  itunitc1  8581  hsmexlem4  8590  hsmexlem5  8591  axdc4lem  8616  pwfseqlem1  8817  eltsk2g  8910  ixxssxr  11304  ioof  11379  fzof  11542  hashbclem  12197  incexclem  13291  ramub1lem1  14079  ramub1lem2  14080  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  submrc  14558  isacs2  14583  isssc  14725  homaf  14890  catcfuccl  14969  catcxpccl  15009  clatl  15278  fpwipodrs  15326  isacs4lem  15330  isacs5lem  15331  dprd2dlem1  16530  ablfac1b  16561  cssval  18087  tgdom  18563  distop  18580  fctop  18588  cctop  18590  ppttop  18591  pptbas  18592  epttop  18593  mretopd  18676  resttopon  18745  dishaus  18966  discmp  18981  cmpsublem  18982  cmpsub  18983  bwthOLD  18994  concompid  19015  2ndcsep  19043  cldllycmp  19079  dislly  19081  iskgen3  19102  kgencn2  19110  txuni2  19118  dfac14  19171  prdstopn  19181  txcmplem1  19194  txcmplem2  19195  hmphdis  19349  fbssfi  19390  trfbas2  19396  uffixsn  19478  hauspwpwf1  19540  alexsubALTlem2  19600  met1stc  20076  restmetu  20142  icccmplem1  20379  icccmplem2  20380  opnmbllem  21061  sqff1o  22500  umgra1  23228  uslgra1  23259  usgraedgrnv  23264  usgrarnedg  23271  usgraedg4  23273  usgrares1  23291  cusgrarn  23335  eupath2  23569  sspval  24089  esumpcvgval  26496  esumcvg  26504  pwsiga  26542  difelsiga  26545  sigainb  26548  measssd  26598  cntnevol  26611  ddemeas  26621  mbfmcnt  26652  br2base  26653  sxbrsigalem0  26655  oms0  26679  probun  26771  coinfliprv  26834  coinflippv  26835  ballotth  26889  cvmcov2  27133  elfuns  27915  altxpsspw  27977  elhf2  28182  opnmbllem0  28398  neibastop1  28551  neibastop2lem  28552  heiborlem1  28681  heiborlem8  28688  elrfi  29001  ismrcd2  29006  istopclsd  29007  mrefg2  29014  isnacs3  29017  dfac11  29386  islssfg2  29395  lnr2i  29443  stoweidlem57  29823  trsspwALT  31481  trsspwALT2  31482  trsspwALT3  31483  pwtrVD  31489  pclfinN  33437  mapd1o  35186
  Copyright terms: Public domain W3C validator