Theorem elpwg 3935

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4528. (Contributed by NM, 6-Aug-2000.)

Assertion

Ref	Expression
elpwg	|- ( A e. V -> ( A e. ~P B <-> A C_ B ) )

Proof of Theorem elpwg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2454	. 2 |- ( x = A -> ( x e. ~P B <-> A e. ~P B ) )
2		sseq1 3438	. 2 |- ( x = A -> ( x C_ B <-> A C_ B ) )
3		selpw 3934	. 2 |- ( x e. ~P B <-> x C_ B )
4	1, 2, 3	vtoclbg 3093	1 |- ( A e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1826   C_ wss 3389   ~Pcpw 3927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403  df-pw 3929

This theorem is referenced by:  elpwi  3936  pwidg  3940  elpwunsn  3985  prsspwg  4101  elpw2g  4528  pwel  4614  f1opw2  6427  eldifpw  6511  elpwun  6512  elpmg  7353  fopwdom  7544  elfpw  7737  f1opwfi  7739  rankwflemb  8124  r1elwf  8127  r1pw  8176  ackbij1lem3  8515  ackbij1lem6  8518  ackbij1lem11  8523  mreexexlemd  15051  acsfn  15066  evls1val  18470  evls1rhm  18472  evls1sca  18473  fiinopn  19495  clsval2  19636  ssntr  19644  neipeltop  19716  nrmsep3  19942  cnrmi  19947  cmpcov  19975  cmpsublem  19985  concompss  20019  kgeni  20123  tgqtop  20298  filss  20439  ufileu  20505  filufint  20506  ustssel  20793  elutop  20821  ustuqtop0  20828  metustssOLD  21141  metustss  21142  metutopOLD  21170  psmetutop  21171  axtgcont1  23982  issubgo  25422  sselpwd  27538  elpwincl1  27539  elpwdifcl  27540  elpwiuncl  27541  crefi  28004  dispcmp  28016  pcmplfin  28017  indval  28162  isrnsigaOLD  28261  sigaclci  28281  sigainb  28285  elsigagen2  28297  sigapildsys  28307  measvunilem  28339  measdivcstOLD  28351  ddeval1  28362  ddeval0  28363  omsfval  28421  omssubaddlem  28426  omssubadd  28427  elcarsg  28432  limsucncmpi  30063  ismrcd1  30796  dvnprodlem1  31909  dvnprodlem2  31910  stoweidlem50  31998  stoweidlem57  32005  elpwdifsn  32617  gsumlsscl  33176  lincfsuppcl  33214  linccl  33215  lincdifsn  33225  lincellss  33227  ellcoellss  33236  lindslinindsimp1  33258  lindslinindimp2lem4  33262  lindslinindsimp2lem5  33263  lindslinindsimp2  33264  lincresunit3lem2  33281  lincresunit3  33282  elpwgded  33677  snelpwrVD  33977  elpwgdedVD  34064  sspwimpcf  34067  sspwimpcfVD  34068  sspwimpALT2  34075