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

Theorem elpw 3633
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 3201 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3629 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2919 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1686   _Vcvv 2790    C_ wss 3154   ~Pcpw 3627
This theorem is referenced by:  elpwg  3634  prsspw  3787  pwpr  3825  pwtp  3826  pwv  3828  sspwuni  3989  iinpw  3992  iunpwss  3993  0elpw  4182  pwuni  4208  snelpwi  4222  snelpw  4223  sspwb  4225  ssextss  4229  pwin  4299  pwunss  4300  pwssun  4301  pwundifOLD  4303  iunpw  4572  ordpwsuc  4608  xpsspw  4799  xpsspwOLD  4800  fabexg  5424  knatar  5859  sorpsscmpl  6290  qsss  6722  mapval2  6799  pmsspw  6804  uniixp  6841  fopwdom  6972  ssenen  7037  fineqvlem  7079  fissuni  7162  fipreima  7163  fival  7168  fiin  7177  fipwuni  7181  dffi3  7186  marypha1lem  7188  hartogslem1  7259  inf3lem6  7336  tz9.12lem3  7463  rankonidlem  7502  tskwe  7585  r0weon  7642  infpwfien  7691  dfac5lem4  7755  dfac2  7759  dfac12lem2  7772  ackbij2lem3  7869  cfval2  7888  fin23lem11  7945  enfin2i  7949  compsscnvlem  7998  isfin1-3  8014  fin1a2lem13  8040  itunitc1  8048  hsmexlem4  8057  hsmexlem5  8058  axdc3lem  8078  axdc4lem  8083  fpwwe2lem1  8255  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe  8270  canthwe  8275  pwfseqlem1  8282  eltsk2g  8375  axgroth5  8448  axgroth6  8452  wuncn  8794  ixxssxr  10670  ioof  10743  fzof  10874  hashbclem  11392  incexclem  12297  vdwmc  13027  ramub2  13063  ram0  13071  ramub1lem1  13075  ramub1lem2  13076  restsspw  13338  prdsplusg  13360  prdsmulr  13361  prdsvsca  13362  ismred  13506  mremre  13508  submrc  13532  isacs2  13557  mreacs  13562  acsfn  13563  isssc  13699  homaf  13864  catcfuccl  13943  catcxpccl  13983  isdrs2  14075  fpwipodrs  14269  isacs4lem  14273  isacs5lem  14274  submacs  14444  subgacs  14654  nsgacs  14655  sylow2alem2  14931  sylow2a  14932  sylow3lem3  14942  sylow3lem6  14945  dprdres  15265  subgdmdprd  15271  dprd2dlem1  15278  ablfac1b  15307  pgpfac1lem5  15316  subrgmre  15571  subsubrg2  15574  lssintcl  15723  lssmre  15725  lssacs  15726  cssval  16584  cssmre  16595  istopon  16665  tgval2  16696  tgdom  16718  distop  16735  fctop  16743  cctop  16745  ppttop  16746  pptbas  16747  epttop  16748  cldss2  16769  ntreq0  16816  discld  16828  mretopd  16831  toponmre  16832  neisspw  16846  resttopon  16894  restdis  16911  cnntr  17006  isnrm2  17088  dishaus  17112  cmpcovf  17120  fincmp  17122  discmp  17127  cmpsublem  17128  cmpsub  17129  cmpcld  17131  cmpfi  17137  concompid  17159  is1stc2  17170  2ndcdisj  17184  2ndcsep  17187  llyi  17202  nllyi  17203  nlly2i  17204  llynlly  17205  subislly  17209  restnlly  17210  llyrest  17213  llyidm  17216  nllyidm  17217  cldllycmp  17223  dislly  17225  iskgen3  17246  kgencn2  17254  txuni2  17262  ptuni2  17273  dfac14  17314  prdstopn  17324  txcmplem1  17337  txcmplem2  17338  qtoptop2  17392  qtopuni  17395  tgqtop  17405  hmphdis  17489  isfbas2  17532  fbssfi  17534  trfbas2  17540  isfild  17555  elfg  17568  cfinfil  17590  csdfil  17591  supfil  17592  isufil2  17605  filssufilg  17608  uffix  17618  uffixsn  17622  ufildr  17628  fin1aufil  17629  hauspwpwf1  17684  alexsubb  17742  alexsubALTlem1  17743  alexsubALTlem2  17744  alexsubALT  17747  ptcmplem5  17752  cldsubg  17795  met1stc  18069  dscopn  18098  icccmplem1  18329  icccmplem2  18330  opnmbllem  18958  vitali  18970  sqff1o  20422  sspval  21301  shex  21793  dfch2  21988  ballotlem2  23049  ballotth  23098  cntnevol  23177  esumel  23428  esumpcvgval  23448  esumcvg  23456  insiga  23500  measssd  23545  mbfmcnt  23575  br2base  23576  coinfliplem  23681  coinflippv  23686  erdszelem7  23730  erdsze2lem2  23737  rellyscon  23784  cvmcov2  23808  umgra1  23880  eupath2  23906  dffr5  24112  elfuns  24456  altxpsspw  24513  elhf2  24807  svs2  25498  sallnei  25540  qusp  25553  fgsb2  25566  bwt2  25603  intvconlem1  25714  issubcata  25857  tartarmap  25899  pgapspf  26063  islocfin  26307  neibastop1  26319  neibastop2lem  26320  neibastop3  26322  topmeet  26324  topjoin  26325  neifg  26331  heibor1lem  26544  heiborlem1  26546  heiborlem8  26553  elrfi  26780  ismrcd1  26784  ismrcd2  26785  istopclsd  26786  mrefg2  26793  isnacs3  26796  pw2f1ocnv  27141  dfac11  27171  islssfg2  27180  filnm  27203  lnr2i  27331  hbtlem6  27344  sdrgacs  27520  stoweidlem57  27817  uslgra1  28129  usgra1  28130  usgraedgrnv  28134  trsspwALT  28665  trsspwALT2  28666  trsspwALT3  28667  pwtrVD  28671  pwtrOLD  28672  pclfinN  30162  lcdlss  31882  mapd1o  31911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-pw 3629
  Copyright terms: Public domain W3C validator