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

Theorem elpw 3605
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 3174 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3601 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2892 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2763    C_ wss 3127   ~Pcpw 3599
This theorem is referenced by:  elpwg  3606  prsspw  3759  pwpr  3797  pwtp  3798  pwv  3800  sspwuni  3961  iinpw  3964  iunpwss  3965  0elpw  4152  pwuni  4178  snelpwi  4192  snelpw  4193  sspwb  4195  ssextss  4199  pwin  4269  pwunss  4270  pwssun  4271  pwundifOLD  4273  iunpw  4542  ordpwsuc  4578  xpsspw  4785  xpsspwOLD  4786  fabexg  5360  knatar  5791  sorpsscmpl  6222  qsss  6688  mapval2  6765  pmsspw  6770  uniixp  6807  fopwdom  6938  ssenen  7003  fineqvlem  7045  fissuni  7128  fipreima  7129  fival  7134  fiin  7143  fipwuni  7147  dffi3  7152  marypha1lem  7154  hartogslem1  7225  inf3lem6  7302  tz9.12lem3  7429  rankonidlem  7468  tskwe  7551  r0weon  7608  infpwfien  7657  dfac5lem4  7721  dfac2  7725  dfac12lem2  7738  ackbij2lem3  7835  cfval2  7854  fin23lem11  7911  enfin2i  7915  compsscnvlem  7964  isfin1-3  7980  fin1a2lem13  8006  itunitc1  8014  hsmexlem4  8023  hsmexlem5  8024  axdc3lem  8044  axdc4lem  8049  fpwwe2lem1  8221  fpwwe2lem11  8230  fpwwe2lem12  8231  fpwwe  8236  canthwe  8241  pwfseqlem1  8248  eltsk2g  8341  axgroth5  8414  axgroth6  8418  wuncn  8760  ixxssxr  10635  ioof  10708  fzof  10839  hashbclem  11356  vdwmc  12988  ramub2  13024  ram0  13032  ramub1lem1  13036  ramub1lem2  13037  restsspw  13299  prdsplusg  13321  prdsmulr  13322  prdsvsca  13323  ismred  13467  mremre  13469  submrc  13493  isacs2  13518  mreacs  13523  acsfn  13524  isssc  13660  homaf  13825  catcfuccl  13904  catcxpccl  13944  isdrs2  14036  fpwipodrs  14230  isacs4lem  14234  isacs5lem  14235  submacs  14405  subgacs  14615  nsgacs  14616  sylow2alem2  14892  sylow2a  14893  sylow3lem3  14903  sylow3lem6  14906  dprdres  15226  subgdmdprd  15232  dprd2dlem1  15239  ablfac1b  15268  pgpfac1lem5  15277  subrgmre  15532  subsubrg2  15535  lssintcl  15684  lssmre  15686  lssacs  15687  cssval  16545  cssmre  16556  istopon  16626  tgval2  16657  tgdom  16679  distop  16696  fctop  16704  cctop  16706  ppttop  16707  pptbas  16708  epttop  16709  cldss2  16730  ntreq0  16777  discld  16789  mretopd  16792  toponmre  16793  neisspw  16807  resttopon  16855  restdis  16872  cnntr  16967  isnrm2  17049  dishaus  17073  cmpcovf  17081  fincmp  17083  discmp  17088  cmpsublem  17089  cmpsub  17090  cmpcld  17092  cmpfi  17098  concompid  17120  is1stc2  17131  2ndcdisj  17145  2ndcsep  17148  llyi  17163  nllyi  17164  nlly2i  17165  llynlly  17166  subislly  17170  restnlly  17171  llyrest  17174  llyidm  17177  nllyidm  17178  cldllycmp  17184  dislly  17186  iskgen3  17207  kgencn2  17215  txuni2  17223  ptuni2  17234  dfac14  17275  prdstopn  17285  txcmplem1  17298  txcmplem2  17299  qtoptop2  17353  qtopuni  17356  tgqtop  17366  hmphdis  17450  isfbas2  17493  fbssfi  17495  trfbas2  17501  isfild  17516  elfg  17529  cfinfil  17551  csdfil  17552  supfil  17553  isufil2  17566  filssufilg  17569  uffix  17579  uffixsn  17583  ufildr  17589  fin1aufil  17590  hauspwpwf1  17645  alexsubb  17703  alexsubALTlem1  17704  alexsubALTlem2  17705  alexsubALT  17708  ptcmplem5  17713  cldsubg  17756  met1stc  18030  dscopn  18059  icccmplem1  18290  icccmplem2  18291  opnmbllem  18919  vitali  18931  sqff1o  20383  sspval  21260  shex  21752  dfch2  21947  ballotlem2  23009  ballotth  23058  erdszelem7  23101  erdsze2lem2  23108  rellyscon  23155  cvmcov2  23179  umgra1  23251  eupath2  23277  dffr5  23482  elfuns  23830  altxpsspw  23887  elhf2  24181  svs2  24855  sallnei  24897  qusp  24910  fgsb2  24923  bwt2  24960  intvconlem1  25071  issubcata  25214  tartarmap  25256  pgapspf  25420  islocfin  25664  neibastop1  25676  neibastop2lem  25677  neibastop3  25679  topmeet  25681  topjoin  25682  neifg  25688  heibor1lem  25901  heiborlem1  25903  heiborlem8  25910  elrfi  26137  ismrcd1  26141  ismrcd2  26142  istopclsd  26143  mrefg2  26150  isnacs3  26153  pw2f1ocnv  26498  dfac11  26528  islssfg2  26537  filnm  26560  lnr2i  26688  hbtlem6  26701  sdrgacs  26877  stoweidlem57  27175  trsspwALT  27725  trsspwALT2  27726  trsspwALT3  27727  pwtrVD  27731  pwtrOLD  27732  pclfinN  29339  lcdlss  31059  mapd1o  31088
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-pw 3601
  Copyright terms: Public domain W3C validator