Theorem elpwg 3868

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

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1756   C_ wss 3328   ~Pcpw 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-in 3335  df-ss 3342  df-pw 3862

This theorem is referenced by:  elpwi  3869  pwidg  3873  elpwunsn  3917  prsspwg  4030  elpw2g  4455  pwel  4544  f1opw2  6313  eldifpw  6388  elpwun  6389  elpmg  7228  fopwdom  7419  elfpw  7613  f1opwfi  7615  rankwflemb  8000  r1elwf  8003  r1pw  8052  ackbij1lem3  8391  ackbij1lem6  8394  ackbij1lem11  8399  mreexexlemd  14582  acsfn  14597  evls1val  17755  evls1rhm  17757  evls1sca  17758  fiinopn  18514  clsval2  18654  ssntr  18662  neipeltop  18733  nrmsep3  18959  cnrmi  18964  cmpcov  18992  cmpsublem  19002  concompss  19037  kgeni  19110  tgqtop  19285  filss  19426  ufileu  19492  filufint  19493  ustssel  19780  elutop  19808  ustuqtop0  19815  metustssOLD  20128  metustss  20129  metutopOLD  20157  psmetutop  20158  axtgcont1  22929  issubgo  23790  fpwrelmap  26033  indval  26470  isrnsigaOLD  26555  sigaclci  26575  sigainb  26579  elsigagen2  26591  measvunilem  26626  measdivcstOLD  26638  ddeval1  26650  ddeval0  26651  omsfval  26709  limsucncmpi  28291  ismrcd1  29034  stoweidlem50  29845  stoweidlem57  29852  gsumlsscl  30814  lincfsuppcl  30947  linccl  30948  lincdifsn  30958  lincellss  30960  ellcoellss  30969  lindslinindsimp1  30991  lindslinindimp2lem4  30995  lindslinindsimp2lem5  30996  lindslinindsimp2  30997  lincresunit3lem2  31014  lincresunit3  31015  elpwgded  31273  snelpwrVD  31567  elpwgdedVD  31653  sspwimpcf  31656  sspwimpcfVD  31657  sspwimpALT2  31664