Theorem elpwg 4018

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4610. (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 2539	. 2 |- ( x = A -> ( x e. ~P B <-> A e. ~P B ) )
2		sseq1 3525	. 2 |- ( x = A -> ( x C_ B <-> A C_ B ) )
3		selpw 4017	. 2 |- ( x e. ~P B <-> x C_ B )
4	1, 2, 3	vtoclbg 3172	1 |- ( A e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1767   C_ wss 3476   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  elpwi  4019  pwidg  4023  elpwunsn  4068  prsspwg  4184  elpw2g  4610  pwel  4699  f1opw2  6512  eldifpw  6596  elpwun  6597  elpmg  7434  fopwdom  7625  elfpw  7822  f1opwfi  7824  rankwflemb  8211  r1elwf  8214  r1pw  8263  ackbij1lem3  8602  ackbij1lem6  8605  ackbij1lem11  8610  mreexexlemd  14899  acsfn  14914  evls1val  18156  evls1rhm  18158  evls1sca  18159  fiinopn  19205  clsval2  19345  ssntr  19353  neipeltop  19424  nrmsep3  19650  cnrmi  19655  cmpcov  19683  cmpsublem  19693  concompss  19728  kgeni  19801  tgqtop  19976  filss  20117  ufileu  20183  filufint  20184  ustssel  20471  elutop  20499  ustuqtop0  20506  metustssOLD  20819  metustss  20820  metutopOLD  20848  psmetutop  20849  axtgcont1  23621  issubgo  25009  fpwrelmap  27256  indval  27695  isrnsigaOLD  27780  sigaclci  27800  sigainb  27804  elsigagen2  27816  measvunilem  27851  measdivcstOLD  27863  ddeval1  27874  ddeval0  27875  omsfval  27933  limsucncmpi  29515  ismrcd1  30262  stoweidlem50  31378  stoweidlem57  31385  elpwdifsn  31791  gsumlsscl  32075  lincfsuppcl  32113  linccl  32114  lincdifsn  32124  lincellss  32126  ellcoellss  32135  lindslinindsimp1  32157  lindslinindimp2lem4  32161  lindslinindsimp2lem5  32162  lindslinindsimp2  32163  lincresunit3lem2  32180  lincresunit3  32181  elpwgded  32435  snelpwrVD  32729  elpwgdedVD  32815  sspwimpcf  32818  sspwimpcfVD  32819  sspwimpALT2  32826