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

Theorem elpw 3765
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 3329 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3761 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3045 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   _Vcvv 2916    C_ wss 3280   ~Pcpw 3759
This theorem is referenced by:  elpwg  3766  prsspw  3931  pwpr  3971  pwtp  3972  pwv  3974  sspwuni  4136  iinpw  4139  iunpwss  4140  0elpw  4329  pwuni  4355  snelpwi  4369  snelpw  4370  prelpwi  4371  sspwb  4373  ssextss  4377  pwin  4447  pwunss  4448  pwssun  4449  iunpw  4718  ordpwsuc  4754  xpsspw  4945  xpsspwOLD  4946  fabexg  5583  knatar  6039  sorpsscmpl  6492  qsss  6924  mapval2  7002  pmsspw  7007  uniixp  7044  ssenen  7240  fineqvlem  7282  fissuni  7369  fipreima  7370  fival  7375  fiin  7385  fipwuni  7389  dffi3  7394  marypha1lem  7396  hartogslem1  7467  inf3lem6  7544  tz9.12lem3  7671  rankonidlem  7710  tskwe  7793  r0weon  7850  infpwfien  7899  dfac5lem4  7963  dfac2  7967  dfac12lem2  7980  cfval2  8096  enfin2i  8157  compsscnvlem  8206  isfin1-3  8222  fin1a2lem13  8248  itunitc1  8256  hsmexlem4  8265  hsmexlem5  8266  axdc3lem  8286  axdc4lem  8291  fpwwe2lem1  8462  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe  8477  canthwe  8482  pwfseqlem1  8489  eltsk2g  8582  axgroth5  8655  axgroth6  8659  wuncn  9001  ixxssxr  10884  ioof  10958  fzof  11092  hashbclem  11656  incexclem  12571  vdwmc  13301  ramub2  13337  ram0  13345  ramub1lem1  13349  ramub1lem2  13350  restsspw  13614  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  ismred  13782  mremre  13784  submrc  13808  isacs2  13833  mreacs  13838  acsfn  13839  isssc  13975  homaf  14140  catcfuccl  14219  catcxpccl  14259  fpwipodrs  14545  isacs4lem  14549  isacs5lem  14550  submacs  14720  subgacs  14930  nsgacs  14931  sylow2alem2  15207  sylow2a  15208  sylow3lem3  15218  sylow3lem6  15221  dprdres  15541  subgdmdprd  15547  dprd2dlem1  15554  ablfac1b  15583  pgpfac1lem5  15592  subrgmre  15847  subsubrg2  15850  lssintcl  15995  lssmre  15997  lssacs  15998  cssval  16864  cssmre  16875  istopon  16945  tgval2  16976  tgdom  16998  distop  17015  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  epttop  17028  cldss2  17049  ntreq0  17096  discld  17108  mretopd  17111  toponmre  17112  neisspw  17126  resttopon  17179  restdis  17196  cnntr  17293  isnrm2  17376  dishaus  17400  cmpcovf  17408  fincmp  17410  discmp  17415  cmpsublem  17416  cmpsub  17417  cmpcld  17419  cmpfi  17425  concompid  17447  is1stc2  17458  2ndcdisj  17472  2ndcsep  17475  llyi  17490  nllyi  17491  nlly2i  17492  llynlly  17493  subislly  17497  restnlly  17498  llyrest  17501  llyidm  17504  nllyidm  17505  cldllycmp  17511  dislly  17513  iskgen3  17534  kgencn2  17542  txuni2  17550  ptuni2  17561  dfac14  17603  prdstopn  17613  txcmplem1  17626  txcmplem2  17627  qtoptop2  17684  qtopuni  17687  tgqtop  17697  hmphdis  17781  isfbas2  17820  fbssfi  17822  trfbas2  17828  isfild  17843  elfg  17856  cfinfil  17878  csdfil  17879  supfil  17880  isufil2  17893  filssufilg  17896  uffix  17906  uffixsn  17910  ufildr  17916  fin1aufil  17917  hauspwpwf1  17972  alexsubb  18030  alexsubALTlem1  18031  alexsubALTlem2  18032  alexsubALT  18035  ptcmplem5  18040  cldsubg  18093  ustfn  18184  ustn0  18203  met1stc  18504  restmetu  18570  dscopn  18574  icccmplem1  18806  icccmplem2  18807  opnmbllem  19446  vitali  19458  sqff1o  20918  umgra1  21314  uslgra1  21345  usgraedgrnv  21350  usgrarnedg  21357  usgraedg4  21359  usgrares1  21377  cusgrarn  21421  eupath2  21655  sspval  22175  shex  22667  dfch2  22862  ishashinf  24112  esumpcvgval  24421  esumcvg  24429  sigaex  24445  sigaval  24446  pwsiga  24466  difelsiga  24469  sigainb  24472  insiga  24473  measssd  24522  measdivcst  24532  cntnevol  24535  mbfmcnt  24571  br2base  24572  sxbrsigalem0  24574  probun  24630  coinfliprv  24693  ballotlem2  24699  ballotth  24748  erdszelem7  24836  erdsze2lem2  24843  rellyscon  24891  cvmcov2  24915  dffr5  25324  elfuns  25668  altxpsspw  25726  elhf2  26020  islocfin  26266  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  topmeet  26283  topjoin  26284  neifg  26290  heibor1lem  26408  heiborlem1  26410  heiborlem8  26417  elrfi  26638  ismrcd1  26642  ismrcd2  26643  istopclsd  26644  mrefg2  26651  isnacs3  26654  pw2f1ocnv  26998  dfac11  27028  islssfg2  27037  filnm  27060  lnr2i  27188  hbtlem6  27201  sdrgacs  27377  stoweidlem57  27673  trsspwALT  28640  trsspwALT2  28641  trsspwALT3  28642  pwtrVD  28646  pclfinN  30382  lcdlss  32102  mapd1o  32131
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761
  Copyright terms: Public domain W3C validator