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

Theorem elpw 3644
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 3212 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3640 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2930 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1696   _Vcvv 2801    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  elpwg  3645  prsspw  3801  pwpr  3839  pwtp  3840  pwv  3842  sspwuni  4003  iinpw  4006  iunpwss  4007  0elpw  4196  pwuni  4222  snelpwi  4236  snelpw  4237  sspwb  4239  ssextss  4243  pwin  4313  pwunss  4314  pwssun  4315  pwundifOLD  4317  iunpw  4586  ordpwsuc  4622  xpsspw  4813  xpsspwOLD  4814  fabexg  5438  knatar  5873  sorpsscmpl  6304  qsss  6736  mapval2  6813  pmsspw  6818  uniixp  6855  fopwdom  6986  ssenen  7051  fineqvlem  7093  fissuni  7176  fipreima  7177  fival  7182  fiin  7191  fipwuni  7195  dffi3  7200  marypha1lem  7202  hartogslem1  7273  inf3lem6  7350  tz9.12lem3  7477  rankonidlem  7516  tskwe  7599  r0weon  7656  infpwfien  7705  dfac5lem4  7769  dfac2  7773  dfac12lem2  7786  ackbij2lem3  7883  cfval2  7902  fin23lem11  7959  enfin2i  7963  compsscnvlem  8012  isfin1-3  8028  fin1a2lem13  8054  itunitc1  8062  hsmexlem4  8071  hsmexlem5  8072  axdc3lem  8092  axdc4lem  8097  fpwwe2lem1  8269  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe  8284  canthwe  8289  pwfseqlem1  8296  eltsk2g  8389  axgroth5  8462  axgroth6  8466  wuncn  8808  ixxssxr  10684  ioof  10757  fzof  10888  hashbclem  11406  incexclem  12311  vdwmc  13041  ramub2  13077  ram0  13085  ramub1lem1  13089  ramub1lem2  13090  restsspw  13352  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  ismred  13520  mremre  13522  submrc  13546  isacs2  13571  mreacs  13576  acsfn  13577  isssc  13713  homaf  13878  catcfuccl  13957  catcxpccl  13997  isdrs2  14089  fpwipodrs  14283  isacs4lem  14287  isacs5lem  14288  submacs  14458  subgacs  14668  nsgacs  14669  sylow2alem2  14945  sylow2a  14946  sylow3lem3  14956  sylow3lem6  14959  dprdres  15279  subgdmdprd  15285  dprd2dlem1  15292  ablfac1b  15321  pgpfac1lem5  15330  subrgmre  15585  subsubrg2  15588  lssintcl  15737  lssmre  15739  lssacs  15740  cssval  16598  cssmre  16609  istopon  16679  tgval2  16710  tgdom  16732  distop  16749  fctop  16757  cctop  16759  ppttop  16760  pptbas  16761  epttop  16762  cldss2  16783  ntreq0  16830  discld  16842  mretopd  16845  toponmre  16846  neisspw  16860  resttopon  16908  restdis  16925  cnntr  17020  isnrm2  17102  dishaus  17126  cmpcovf  17134  fincmp  17136  discmp  17141  cmpsublem  17142  cmpsub  17143  cmpcld  17145  cmpfi  17151  concompid  17173  is1stc2  17184  2ndcdisj  17198  2ndcsep  17201  llyi  17216  nllyi  17217  nlly2i  17218  llynlly  17219  subislly  17223  restnlly  17224  llyrest  17227  llyidm  17230  nllyidm  17231  cldllycmp  17237  dislly  17239  iskgen3  17260  kgencn2  17268  txuni2  17276  ptuni2  17287  dfac14  17328  prdstopn  17338  txcmplem1  17351  txcmplem2  17352  qtoptop2  17406  qtopuni  17409  tgqtop  17419  hmphdis  17503  isfbas2  17546  fbssfi  17548  trfbas2  17554  isfild  17569  elfg  17582  cfinfil  17604  csdfil  17605  supfil  17606  isufil2  17619  filssufilg  17622  uffix  17632  uffixsn  17636  ufildr  17642  fin1aufil  17643  hauspwpwf1  17698  alexsubb  17756  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALT  17761  ptcmplem5  17766  cldsubg  17809  met1stc  18083  dscopn  18112  icccmplem1  18343  icccmplem2  18344  opnmbllem  18972  vitali  18984  sqff1o  20436  sspval  21315  shex  21807  dfch2  22002  ballotlem2  23063  ballotth  23112  cntnevol  23191  esumel  23441  esumpcvgval  23461  esumcvg  23469  insiga  23513  measssd  23558  mbfmcnt  23588  br2base  23589  coinfliplem  23694  coinflippv  23699  erdszelem7  23743  erdsze2lem2  23750  rellyscon  23797  cvmcov2  23821  umgra1  23893  eupath2  23919  dffr5  24181  elfuns  24525  altxpsspw  24583  elhf2  24877  svs2  25590  sallnei  25632  qusp  25645  fgsb2  25658  bwt2  25695  intvconlem1  25806  issubcata  25949  tartarmap  25991  pgapspf  26155  islocfin  26399  neibastop1  26411  neibastop2lem  26412  neibastop3  26414  topmeet  26416  topjoin  26417  neifg  26423  heibor1lem  26636  heiborlem1  26638  heiborlem8  26645  elrfi  26872  ismrcd1  26876  ismrcd2  26877  istopclsd  26878  mrefg2  26885  isnacs3  26888  pw2f1ocnv  27233  dfac11  27263  islssfg2  27272  filnm  27295  lnr2i  27423  hbtlem6  27436  sdrgacs  27612  stoweidlem57  27909  uslgra1  28252  usgra1  28253  usgraedgrnv  28257  trsspwALT  28908  trsspwALT2  28909  trsspwALT3  28910  pwtrVD  28914  pwtrOLD  28915  pclfinN  30711  lcdlss  32431  mapd1o  32460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator