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

Theorem elpw 3632
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 3200 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3628 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2918 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1685   _Vcvv 2789    C_ wss 3153   ~Pcpw 3626
This theorem is referenced by:  elpwg  3633  prsspw  3786  pwpr  3824  pwtp  3825  pwv  3827  sspwuni  3988  iinpw  3991  iunpwss  3992  0elpw  4179  pwuni  4205  snelpwi  4219  snelpw  4220  sspwb  4222  ssextss  4226  pwin  4296  pwunss  4297  pwssun  4298  pwundifOLD  4300  iunpw  4569  ordpwsuc  4605  xpsspw  4796  xpsspwOLD  4797  fabexg  5388  knatar  5819  sorpsscmpl  6250  qsss  6716  mapval2  6793  pmsspw  6798  uniixp  6835  fopwdom  6966  ssenen  7031  fineqvlem  7073  fissuni  7156  fipreima  7157  fival  7162  fiin  7171  fipwuni  7175  dffi3  7180  marypha1lem  7182  hartogslem1  7253  inf3lem6  7330  tz9.12lem3  7457  rankonidlem  7496  tskwe  7579  r0weon  7636  infpwfien  7685  dfac5lem4  7749  dfac2  7753  dfac12lem2  7766  ackbij2lem3  7863  cfval2  7882  fin23lem11  7939  enfin2i  7943  compsscnvlem  7992  isfin1-3  8008  fin1a2lem13  8034  itunitc1  8042  hsmexlem4  8051  hsmexlem5  8052  axdc3lem  8072  axdc4lem  8077  fpwwe2lem1  8249  fpwwe2lem11  8258  fpwwe2lem12  8259  fpwwe  8264  canthwe  8269  pwfseqlem1  8276  eltsk2g  8369  axgroth5  8442  axgroth6  8446  wuncn  8788  ixxssxr  10664  ioof  10737  fzof  10868  hashbclem  11386  incexclem  12291  vdwmc  13021  ramub2  13057  ram0  13065  ramub1lem1  13069  ramub1lem2  13070  restsspw  13332  prdsplusg  13354  prdsmulr  13355  prdsvsca  13356  ismred  13500  mremre  13502  submrc  13526  isacs2  13551  mreacs  13556  acsfn  13557  isssc  13693  homaf  13858  catcfuccl  13937  catcxpccl  13977  isdrs2  14069  fpwipodrs  14263  isacs4lem  14267  isacs5lem  14268  submacs  14438  subgacs  14648  nsgacs  14649  sylow2alem2  14925  sylow2a  14926  sylow3lem3  14936  sylow3lem6  14939  dprdres  15259  subgdmdprd  15265  dprd2dlem1  15272  ablfac1b  15301  pgpfac1lem5  15310  subrgmre  15565  subsubrg2  15568  lssintcl  15717  lssmre  15719  lssacs  15720  cssval  16578  cssmre  16589  istopon  16659  tgval2  16690  tgdom  16712  distop  16729  fctop  16737  cctop  16739  ppttop  16740  pptbas  16741  epttop  16742  cldss2  16763  ntreq0  16810  discld  16822  mretopd  16825  toponmre  16826  neisspw  16840  resttopon  16888  restdis  16905  cnntr  17000  isnrm2  17082  dishaus  17106  cmpcovf  17114  fincmp  17116  discmp  17121  cmpsublem  17122  cmpsub  17123  cmpcld  17125  cmpfi  17131  concompid  17153  is1stc2  17164  2ndcdisj  17178  2ndcsep  17181  llyi  17196  nllyi  17197  nlly2i  17198  llynlly  17199  subislly  17203  restnlly  17204  llyrest  17207  llyidm  17210  nllyidm  17211  cldllycmp  17217  dislly  17219  iskgen3  17240  kgencn2  17248  txuni2  17256  ptuni2  17267  dfac14  17308  prdstopn  17318  txcmplem1  17331  txcmplem2  17332  qtoptop2  17386  qtopuni  17389  tgqtop  17399  hmphdis  17483  isfbas2  17526  fbssfi  17528  trfbas2  17534  isfild  17549  elfg  17562  cfinfil  17584  csdfil  17585  supfil  17586  isufil2  17599  filssufilg  17602  uffix  17612  uffixsn  17616  ufildr  17622  fin1aufil  17623  hauspwpwf1  17678  alexsubb  17736  alexsubALTlem1  17737  alexsubALTlem2  17738  alexsubALT  17741  ptcmplem5  17746  cldsubg  17789  met1stc  18063  dscopn  18092  icccmplem1  18323  icccmplem2  18324  opnmbllem  18952  vitali  18964  sqff1o  20416  sspval  21293  shex  21787  dfch2  21982  ballotlem2  23043  ballotth  23092  erdszelem7  23135  erdsze2lem2  23142  rellyscon  23189  cvmcov2  23213  umgra1  23285  eupath2  23311  dffr5  23516  elfuns  23864  altxpsspw  23921  elhf2  24215  svs2  24898  sallnei  24940  qusp  24953  fgsb2  24966  bwt2  25003  intvconlem1  25114  issubcata  25257  tartarmap  25299  pgapspf  25463  islocfin  25707  neibastop1  25719  neibastop2lem  25720  neibastop3  25722  topmeet  25724  topjoin  25725  neifg  25731  heibor1lem  25944  heiborlem1  25946  heiborlem8  25953  elrfi  26180  ismrcd1  26184  ismrcd2  26185  istopclsd  26186  mrefg2  26193  isnacs3  26196  pw2f1ocnv  26541  dfac11  26571  islssfg2  26580  filnm  26603  lnr2i  26731  hbtlem6  26744  sdrgacs  26920  stoweidlem57  27217  trsspwALT  27872  trsspwALT2  27873  trsspwALT3  27874  pwtrVD  27878  pwtrOLD  27879  pclfinN  29368  lcdlss  31088  mapd1o  31117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator