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

Theorem elpw 3741
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 3305 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3737 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3021 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1717   _Vcvv 2892    C_ wss 3256   ~Pcpw 3735
This theorem is referenced by:  elpwg  3742  prsspw  3906  pwpr  3946  pwtp  3947  pwv  3949  sspwuni  4110  iinpw  4113  iunpwss  4114  0elpw  4303  pwuni  4329  snelpwi  4343  snelpw  4344  prelpwi  4345  sspwb  4347  ssextss  4351  pwin  4421  pwunss  4422  pwssun  4423  iunpw  4692  ordpwsuc  4728  xpsspw  4919  xpsspwOLD  4920  fabexg  5557  knatar  6012  sorpsscmpl  6462  qsss  6894  mapval2  6972  pmsspw  6977  uniixp  7014  ssenen  7210  fineqvlem  7252  fissuni  7339  fipreima  7340  fival  7345  fiin  7355  fipwuni  7359  dffi3  7364  marypha1lem  7366  hartogslem1  7437  inf3lem6  7514  tz9.12lem3  7641  rankonidlem  7680  tskwe  7763  r0weon  7820  infpwfien  7869  dfac5lem4  7933  dfac2  7937  dfac12lem2  7950  cfval2  8066  enfin2i  8127  compsscnvlem  8176  isfin1-3  8192  fin1a2lem13  8218  itunitc1  8226  hsmexlem4  8235  hsmexlem5  8236  axdc3lem  8256  axdc4lem  8261  fpwwe2lem1  8432  fpwwe2lem11  8441  fpwwe2lem12  8442  fpwwe  8447  canthwe  8452  pwfseqlem1  8459  eltsk2g  8552  axgroth5  8625  axgroth6  8629  wuncn  8971  ixxssxr  10853  ioof  10927  fzof  11060  hashbclem  11621  incexclem  12536  vdwmc  13266  ramub2  13302  ram0  13310  ramub1lem1  13314  ramub1lem2  13315  restsspw  13579  prdsplusg  13601  prdsmulr  13602  prdsvsca  13603  ismred  13747  mremre  13749  submrc  13773  isacs2  13798  mreacs  13803  acsfn  13804  isssc  13940  homaf  14105  catcfuccl  14184  catcxpccl  14224  fpwipodrs  14510  isacs4lem  14514  isacs5lem  14515  submacs  14685  subgacs  14895  nsgacs  14896  sylow2alem2  15172  sylow2a  15173  sylow3lem3  15183  sylow3lem6  15186  dprdres  15506  subgdmdprd  15512  dprd2dlem1  15519  ablfac1b  15548  pgpfac1lem5  15557  subrgmre  15812  subsubrg2  15815  lssintcl  15960  lssmre  15962  lssacs  15963  cssval  16825  cssmre  16836  istopon  16906  tgval2  16937  tgdom  16959  distop  16976  fctop  16984  cctop  16986  ppttop  16987  pptbas  16988  epttop  16989  cldss2  17010  ntreq0  17057  discld  17069  mretopd  17072  toponmre  17073  neisspw  17087  resttopon  17140  restdis  17157  cnntr  17254  isnrm2  17337  dishaus  17361  cmpcovf  17369  fincmp  17371  discmp  17376  cmpsublem  17377  cmpsub  17378  cmpcld  17380  cmpfi  17386  concompid  17408  is1stc2  17419  2ndcdisj  17433  2ndcsep  17436  llyi  17451  nllyi  17452  nlly2i  17453  llynlly  17454  subislly  17458  restnlly  17459  llyrest  17462  llyidm  17465  nllyidm  17466  cldllycmp  17472  dislly  17474  iskgen3  17495  kgencn2  17503  txuni2  17511  ptuni2  17522  dfac14  17564  prdstopn  17574  txcmplem1  17587  txcmplem2  17588  qtoptop2  17645  qtopuni  17648  tgqtop  17658  hmphdis  17742  isfbas2  17781  fbssfi  17783  trfbas2  17789  isfild  17804  elfg  17817  cfinfil  17839  csdfil  17840  supfil  17841  isufil2  17854  filssufilg  17857  uffix  17867  uffixsn  17871  ufildr  17877  fin1aufil  17878  hauspwpwf1  17933  alexsubb  17991  alexsubALTlem1  17992  alexsubALTlem2  17993  alexsubALT  17996  ptcmplem5  18001  cldsubg  18054  ustfn  18145  ustn0  18164  met1stc  18434  restmetu  18482  dscopn  18485  icccmplem1  18717  icccmplem2  18718  opnmbllem  19353  vitali  19365  sqff1o  20825  umgra1  21221  uslgra1  21252  usgraedgrnv  21257  usgrarnedg  21263  usgraedg4  21265  usgrares1  21283  cusgrarn  21327  eupath2  21543  sspval  22063  shex  22555  dfch2  22750  ishashinf  23990  esumpcvgval  24257  esumcvg  24265  sigaex  24281  sigaval  24282  pwsiga  24302  difelsiga  24305  sigainb  24308  insiga  24309  measssd  24356  measdivcst  24366  cntnevol  24369  mbfmcnt  24405  br2base  24406  sxbrsigalem0  24408  probun  24449  coinfliprv  24512  ballotlem2  24518  ballotth  24567  erdszelem7  24655  erdsze2lem2  24662  rellyscon  24710  cvmcov2  24734  dffr5  25127  elfuns  25471  altxpsspw  25529  elhf2  25823  islocfin  26060  neibastop1  26072  neibastop2lem  26073  neibastop3  26075  topmeet  26077  topjoin  26078  neifg  26084  heibor1lem  26202  heiborlem1  26204  heiborlem8  26211  elrfi  26432  ismrcd1  26436  ismrcd2  26437  istopclsd  26438  mrefg2  26445  isnacs3  26448  pw2f1ocnv  26792  dfac11  26822  islssfg2  26831  filnm  26854  lnr2i  26982  hbtlem6  26995  sdrgacs  27171  stoweidlem57  27467  trsspwALT  28265  trsspwALT2  28266  trsspwALT3  28267  pwtrVD  28271  pclfinN  30065  lcdlss  31785  mapd1o  31814
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-in 3263  df-ss 3270  df-pw 3737
  Copyright terms: Public domain W3C validator