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

Theorem elpw 3798
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 3362 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3794 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3078 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1725   _Vcvv 2949    C_ wss 3313   ~Pcpw 3792
This theorem is referenced by:  elpwg  3799  prsspw  3964  pwpr  4004  pwtp  4005  pwv  4007  sspwuni  4169  iinpw  4172  iunpwss  4173  0elpw  4362  pwuni  4388  snelpwi  4402  snelpw  4403  prelpwi  4404  sspwb  4406  ssextss  4410  pwin  4480  pwunss  4481  pwssun  4482  iunpw  4752  ordpwsuc  4788  xpsspw  4979  xpsspwOLD  4980  fabexg  5617  knatar  6073  sorpsscmpl  6526  qsss  6958  mapval2  7036  pmsspw  7041  uniixp  7078  ssenen  7274  fineqvlem  7316  fissuni  7404  fipreima  7405  fival  7410  fiin  7420  fipwuni  7424  dffi3  7429  marypha1lem  7431  hartogslem1  7504  inf3lem6  7581  tz9.12lem3  7708  rankonidlem  7747  tskwe  7830  r0weon  7887  infpwfien  7936  dfac5lem4  8000  dfac2  8004  dfac12lem2  8017  cfval2  8133  enfin2i  8194  compsscnvlem  8243  isfin1-3  8259  fin1a2lem13  8285  itunitc1  8293  hsmexlem4  8302  hsmexlem5  8303  axdc3lem  8323  axdc4lem  8328  fpwwe2lem1  8499  fpwwe2lem11  8508  fpwwe2lem12  8509  fpwwe  8514  canthwe  8519  pwfseqlem1  8526  eltsk2g  8619  axgroth5  8692  axgroth6  8696  wuncn  9038  ixxssxr  10921  ioof  10995  fzof  11130  hashbclem  11694  incexclem  12609  vdwmc  13339  ramub2  13375  ram0  13383  ramub1lem1  13387  ramub1lem2  13388  restsspw  13652  prdsplusg  13674  prdsmulr  13675  prdsvsca  13676  ismred  13820  mremre  13822  submrc  13846  isacs2  13871  mreacs  13876  acsfn  13877  isssc  14013  homaf  14178  catcfuccl  14257  catcxpccl  14297  fpwipodrs  14583  isacs4lem  14587  isacs5lem  14588  submacs  14758  subgacs  14968  nsgacs  14969  sylow2alem2  15245  sylow2a  15246  sylow3lem3  15256  sylow3lem6  15259  dprdres  15579  subgdmdprd  15585  dprd2dlem1  15592  ablfac1b  15621  pgpfac1lem5  15630  subrgmre  15885  subsubrg2  15888  lssintcl  16033  lssmre  16035  lssacs  16036  cssval  16902  cssmre  16913  istopon  16983  tgval2  17014  tgdom  17036  distop  17053  fctop  17061  cctop  17063  ppttop  17064  pptbas  17065  epttop  17066  cldss2  17087  ntreq0  17134  discld  17146  mretopd  17149  toponmre  17150  neisspw  17164  resttopon  17218  restdis  17235  cnntr  17332  isnrm2  17415  dishaus  17439  cmpcovf  17447  fincmp  17449  discmp  17454  cmpsublem  17455  cmpsub  17456  cmpcld  17458  cmpfi  17464  bwth  17466  concompid  17487  is1stc2  17498  2ndcdisj  17512  2ndcsep  17515  llyi  17530  nllyi  17531  nlly2i  17532  llynlly  17533  subislly  17537  restnlly  17538  llyrest  17541  llyidm  17544  nllyidm  17545  cldllycmp  17551  dislly  17553  iskgen3  17574  kgencn2  17582  txuni2  17590  ptuni2  17601  dfac14  17643  prdstopn  17653  txcmplem1  17666  txcmplem2  17667  qtoptop2  17724  qtopuni  17727  tgqtop  17737  hmphdis  17821  isfbas2  17860  fbssfi  17862  trfbas2  17868  isfild  17883  elfg  17896  cfinfil  17918  csdfil  17919  supfil  17920  isufil2  17933  filssufilg  17936  uffix  17946  uffixsn  17950  ufildr  17956  fin1aufil  17957  hauspwpwf1  18012  alexsubb  18070  alexsubALTlem1  18071  alexsubALTlem2  18072  alexsubALT  18075  ptcmplem5  18080  cldsubg  18133  ustfn  18224  ustn0  18243  met1stc  18544  restmetu  18610  dscopn  18614  icccmplem1  18846  icccmplem2  18847  opnmbllem  19486  vitali  19498  sqff1o  20958  umgra1  21354  uslgra1  21385  usgraedgrnv  21390  usgrarnedg  21397  usgraedg4  21399  usgrares1  21417  cusgrarn  21461  eupath2  21695  sspval  22215  shex  22707  dfch2  22902  ishashinf  24152  esumpcvgval  24461  esumcvg  24469  sigaex  24485  sigaval  24486  pwsiga  24506  difelsiga  24509  sigainb  24512  insiga  24513  measssd  24562  measdivcst  24572  cntnevol  24575  mbfmcnt  24611  br2base  24612  sxbrsigalem0  24614  probun  24670  coinfliprv  24733  ballotlem2  24739  ballotth  24788  erdszelem7  24876  erdsze2lem2  24883  rellyscon  24931  cvmcov2  24955  dffr5  25369  elfuns  25753  altxpsspw  25815  elhf2  26109  islocfin  26368  neibastop1  26380  neibastop2lem  26381  neibastop3  26383  topmeet  26385  topjoin  26386  neifg  26392  heibor1lem  26510  heiborlem1  26512  heiborlem8  26519  elrfi  26740  ismrcd1  26744  ismrcd2  26745  istopclsd  26746  mrefg2  26753  isnacs3  26756  pw2f1ocnv  27100  dfac11  27129  islssfg2  27138  filnm  27161  lnr2i  27289  hbtlem6  27302  sdrgacs  27478  stoweidlem57  27774  trsspwALT  28869  trsspwALT2  28870  trsspwALT3  28871  pwtrVD  28875  pclfinN  30635  lcdlss  32355  mapd1o  32384
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-in 3320  df-ss 3327  df-pw 3794
  Copyright terms: Public domain W3C validator