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

Theorem elpw 3536
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
StepHypRef Expression
1 elpw.1 . 2  |-  A  e. 
_V
2 sseq1 3120 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3532 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2854 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2727    C_ wss 3078   ~Pcpw 3530
This theorem is referenced by:  elpwg  3537  prsspw  3685  pwpr  3723  pwtp  3724  pwv  3726  sspwuni  3885  iinpw  3888  iunpwss  3889  0elpw  4074  pwuni  4100  snelpwi  4114  snelpw  4115  sspwb  4117  ssextss  4121  pwin  4190  pwunss  4191  pwssun  4192  pwundifOLD  4194  iunpw  4461  ordpwsuc  4497  xpsspw  4704  xpsspwOLD  4705  fabexg  5279  knatar  5709  sorpsscmpl  6140  qsss  6606  mapval2  6683  pmsspw  6688  uniixp  6725  fopwdom  6855  ssenen  6920  fineqvlem  6962  fissuni  7044  fipreima  7045  fival  7050  fiin  7059  fipwuni  7063  dffi3  7068  marypha1lem  7070  hartogslem1  7141  inf3lem6  7218  tz9.12lem3  7345  rankonidlem  7384  tskwe  7467  r0weon  7524  infpwfien  7573  dfac5lem4  7637  dfac2  7641  dfac12lem2  7654  ackbij2lem3  7751  cfval2  7770  fin23lem11  7827  enfin2i  7831  compsscnvlem  7880  isfin1-3  7896  fin1a2lem13  7922  itunitc1  7930  hsmexlem4  7939  hsmexlem5  7940  axdc3lem  7960  axdc4lem  7965  fpwwe2lem1  8133  fpwwe2lem11  8142  fpwwe2lem12  8143  fpwwe  8148  canthwe  8153  pwfseqlem1  8160  eltsk2g  8253  axgroth5  8326  axgroth6  8330  wuncn  8672  ixxssxr  10546  ioof  10619  fzof  10750  hashbclem  11267  vdwmc  12899  ramub2  12935  ram0  12943  ramub1lem1  12947  ramub1lem2  12948  restsspw  13210  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  ismred  13376  mremre  13378  submrc  13397  isacs2  13400  mreacs  13404  acsfn  13405  isssc  13541  homaf  13706  catcfuccl  13785  catcxpccl  13825  isdrs2  13917  fpwipodrs  14111  isacs4lem  14115  isacs5lem  14116  submacs  14277  subgacs  14487  nsgacs  14488  sylow2alem2  14764  sylow2a  14765  sylow3lem3  14775  sylow3lem6  14778  dprdres  15098  subgdmdprd  15104  dprd2dlem1  15111  ablfac1b  15140  pgpfac1lem5  15149  subrgmre  15404  subsubrg2  15407  lssintcl  15556  lssmre  15558  lssacs  15559  cssval  16414  cssmre  16425  istopon  16495  tgval2  16526  tgdom  16548  distop  16565  fctop  16573  cctop  16575  ppttop  16576  pptbas  16577  epttop  16578  cldss2  16599  ntreq0  16646  discld  16658  mretopd  16661  toponmre  16662  neisspw  16676  resttopon  16724  restdis  16741  cnntr  16836  isnrm2  16918  dishaus  16942  cmpcovf  16950  fincmp  16952  discmp  16957  cmpsublem  16958  cmpsub  16959  cmpcld  16961  cmpfi  16967  concompid  16989  is1stc2  17000  2ndcdisj  17014  2ndcsep  17017  llyi  17032  nllyi  17033  nlly2i  17034  llynlly  17035  subislly  17039  restnlly  17040  llyrest  17043  llyidm  17046  nllyidm  17047  cldllycmp  17053  dislly  17055  iskgen3  17076  kgencn2  17084  txuni2  17092  ptuni2  17103  dfac14  17144  prdstopn  17154  txcmplem1  17167  txcmplem2  17168  qtoptop2  17222  qtopuni  17225  tgqtop  17235  hmphdis  17319  isfbas2  17362  fbssfi  17364  trfbas2  17370  isfild  17385  elfg  17398  cfinfil  17420  csdfil  17421  supfil  17422  isufil2  17435  filssufilg  17438  uffix  17448  uffixsn  17452  ufildr  17458  fin1aufil  17459  hauspwpwf1  17514  alexsubb  17572  alexsubALTlem1  17573  alexsubALTlem2  17574  alexsubALT  17577  ptcmplem5  17582  cldsubg  17625  met1stc  17899  dscopn  17928  icccmplem1  18159  icccmplem2  18160  opnmbllem  18788  vitali  18800  sqff1o  20252  sspval  21129  shex  21621  dfch2  21816  erdszelem7  22899  erdsze2lem2  22906  rellyscon  22953  cvmcov2  22977  umgra1  23049  eupath2  23075  dffr5  23280  elfuns  23628  altxpsspw  23685  elhf2  23979  svs2  24653  sallnei  24695  qusp  24708  fgsb2  24721  bwt2  24758  intvconlem1  24869  issubcata  25012  tartarmap  25054  pgapspf  25218  islocfin  25462  neibastop1  25474  neibastop2lem  25475  neibastop3  25477  topmeet  25479  topjoin  25480  neifg  25486  heibor1lem  25699  heiborlem1  25701  heiborlem8  25708  elrfi  25935  ismrcd1  25939  ismrcd2  25940  istopclsd  25941  mrefg2  25948  isnacs3  25951  pw2f1ocnv  26296  dfac11  26326  islssfg2  26335  filnm  26358  lnr2i  26486  hbtlem6  26499  sdrgacs  26675  trsspwALT  27282  trsspwALT2  27283  trsspwALT3  27284  pwtrVD  27288  pwtrOLD  27289  pclfinN  28890  lcdlss  30610  mapd1o  30639
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator