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

Theorem elpw 4016
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 3525 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 4012 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3253 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   _Vcvv 3113    C_ wss 3476   ~Pcpw 4010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012
This theorem is referenced by:  selpw  4017  prsspw  4199  0elpw  4616  snelpwi  4692  snelpw  4693  prelpwi  4694  sspwb  4696  pwssun  4786  xpsspwOLD  5117  knatar  6241  iunpw  6598  ssenen  7691  fissuni  7825  fipreima  7826  fiin  7882  fipwuni  7886  dffi3  7891  marypha1lem  7893  inf3lem6  8050  tz9.12lem3  8207  rankonidlem  8246  r0weon  8390  infpwfien  8443  dfac5lem4  8507  dfac2  8511  dfac12lem2  8524  enfin2i  8701  isfin1-3  8766  itunitc1  8800  hsmexlem4  8809  hsmexlem5  8810  axdc4lem  8835  pwfseqlem1  9036  eltsk2g  9129  ixxssxr  11541  ioof  11622  fzof  11794  hashbclem  12467  incexclem  13611  ramub1lem1  14403  ramub1lem2  14404  prdsplusg  14713  prdsmulr  14714  prdsvsca  14715  submrc  14883  isacs2  14908  isssc  15050  homaf  15215  catcfuccl  15294  catcxpccl  15334  clatl  15603  fpwipodrs  15651  isacs4lem  15655  isacs5lem  15656  dprd2dlem1  16892  ablfac1b  16923  cssval  18508  tgdom  19274  distop  19291  fctop  19299  cctop  19301  ppttop  19302  pptbas  19303  epttop  19304  mretopd  19387  resttopon  19456  dishaus  19677  discmp  19692  cmpsublem  19693  cmpsub  19694  bwthOLD  19705  concompid  19726  2ndcsep  19754  cldllycmp  19790  dislly  19792  iskgen3  19813  kgencn2  19821  txuni2  19829  dfac14  19882  prdstopn  19892  txcmplem1  19905  txcmplem2  19906  hmphdis  20060  fbssfi  20101  trfbas2  20107  uffixsn  20189  hauspwpwf1  20251  alexsubALTlem2  20311  met1stc  20787  restmetu  20853  icccmplem1  21090  icccmplem2  21091  opnmbllem  21773  sqff1o  23212  umgra1  24030  uslgra1  24076  usgraedgrnv  24081  usgrarnedg  24088  usgraedg4  24091  usgrares1  24114  cusgrarn  24163  eupath2  24684  sspval  25340  esumpcvgval  27752  esumcvg  27760  pwsiga  27798  difelsiga  27801  sigainb  27804  measssd  27854  cntnevol  27867  ddemeas  27876  mbfmcnt  27907  br2base  27908  sxbrsigalem0  27910  oms0  27934  probun  28026  coinfliprv  28089  coinflippv  28090  ballotth  28144  cvmcov2  28388  elfuns  29170  altxpsspw  29232  elhf2  29437  opnmbllem0  29655  neibastop1  29808  neibastop2lem  29809  heiborlem1  29938  heiborlem8  29945  elrfi  30258  ismrcd2  30263  istopclsd  30264  mrefg2  30271  isnacs3  30274  dfac11  30640  islssfg2  30649  lnr2i  30697  stoweidlem57  31385  prelpw  31794  trsspwALT  32714  trsspwALT2  32715  trsspwALT3  32716  pwtrVD  32722  pclfinN  34714  mapd1o  36463
  Copyright terms: Public domain W3C validator