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

Theorem elpw 3969
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 3465 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3965 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3200 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    e. wcel 1898   _Vcvv 3057    C_ wss 3416   ~Pcpw 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-pw 3965
This theorem is referenced by:  selpw  3970  prsspwOLD  4158  0elpw  4586  snelpwi  4659  snelpw  4660  prelpwi  4661  sspwb  4663  pwssun  4759  xpsspw  4967  knatar  6273  iunpw  6632  ssenen  7772  fissuni  7905  fipreima  7906  fiin  7962  fipwuni  7966  dffi3  7971  marypha1lem  7973  inf3lem6  8164  tz9.12lem3  8286  rankonidlem  8325  r0weon  8469  infpwfien  8519  dfac5lem4  8583  dfac2  8587  dfac12lem2  8600  enfin2i  8777  isfin1-3  8842  itunitc1  8876  hsmexlem4  8885  hsmexlem5  8886  axdc4lem  8911  pwfseqlem1  9109  eltsk2g  9202  ixxssxr  11676  ioof  11761  fzof  11948  hashbclem  12648  incexclem  13943  ramub1lem1  15033  ramub1lem2  15034  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  submrc  15583  isacs2  15608  isssc  15774  homaf  15974  catcfuccl  16053  catcxpccl  16141  clatl  16411  fpwipodrs  16459  isacs4lem  16463  isacs5lem  16464  dprd2dlem1  17723  ablfac1b  17752  cssval  19294  tgdom  20043  distop  20060  fctop  20068  cctop  20070  ppttop  20071  pptbas  20072  epttop  20073  mretopd  20157  resttopon  20226  dishaus  20447  discmp  20462  cmpsublem  20463  cmpsub  20464  concompid  20495  2ndcsep  20523  cldllycmp  20559  dislly  20561  iskgen3  20613  kgencn2  20621  txuni2  20629  dfac14  20682  prdstopn  20692  txcmplem1  20705  txcmplem2  20706  hmphdis  20860  fbssfi  20901  trfbas2  20907  uffixsn  20989  hauspwpwf1  21051  alexsubALTlem2  21112  met1stc  21585  restmetu  21634  icccmplem1  21889  icccmplem2  21890  opnmbllem  22608  sqff1o  24158  umgra1  25102  uslgra1  25148  usgraedgrnv  25153  usgrarnedg  25160  usgraedg4  25163  usgrares1  25187  cusgrarn  25236  eupath2  25757  sspval  26411  foresf1o  28188  cmpcref  28726  esumpcvgval  28948  esumcvg  28956  esum2d  28963  pwsiga  29001  difelsiga  29004  sigainb  29007  inelpisys  29025  pwldsys  29028  rossros  29051  measssd  29086  cntnevol  29099  ddemeas  29108  mbfmcnt  29139  br2base  29140  sxbrsigalem0  29142  oms0  29174  oms0OLD  29178  probun  29301  coinfliprv  29364  ballotth  29419  ballotthOLD  29457  cvmcov2  30047  elfuns  30731  altxpsspw  30793  elhf2  30991  neibastop1  31064  neibastop2lem  31065  opnmbllem0  32021  heiborlem1  32188  heiborlem8  32195  pclfinN  33510  mapd1o  35261  elrfi  35581  ismrcd2  35586  istopclsd  35587  mrefg2  35594  isnacs3  35597  dfac11  35965  islssfg2  35974  lnr2i  36020  trsspwALT  37246  trsspwALT2  37247  trsspwALT3  37248  pwtrVD  37260  stoweidlem57  37956  intsal  38227  salexct  38231  sge0resplit  38286  omeiunltfirp  38378  prelpw  39033  incistruhgr  39218  upgr1e  39249  umgredg  39277  uspgr1e  39369  uhgrspansubgrlem  39412
  Copyright terms: Public domain W3C validator