Theorem elpwg 3959

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

Syntax hints:   -> wi 4   <-> wb 188   e. wcel 1887   C_ wss 3404   ~Pcpw 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953

This theorem is referenced by:  elpwi  3960  pwidg  3964  elpwunsn  4012  prsspwg  4129  elpw2g  4566  pwel  4652  f1opw2  6522  eldifpw  6603  elpwun  6604  elpmg  7487  fopwdom  7680  elfpw  7876  f1opwfi  7878  rankwflemb  8264  r1elwf  8267  r1pw  8316  ackbij1lem3  8652  ackbij1lem6  8655  ackbij1lem11  8660  lcmfval  14591  lcmf0val  14592  lcmfvalOLD  14595  mreexexlemd  15550  acsfn  15565  evls1val  18909  evls1rhm  18911  evls1sca  18912  fiinopn  19931  clsval2  20065  ssntr  20073  neipeltop  20145  nrmsep3  20371  cnrmi  20376  cmpcov  20404  cmpsublem  20414  concompss  20448  kgeni  20552  tgqtop  20727  filss  20868  ufileu  20934  filufint  20935  ustssel  21220  elutop  21248  ustuqtop0  21255  metustss  21566  psmetutop  21582  axtgcont1  24516  issubgo  26031  sselpwd  28153  elpwincl1  28154  elpwdifcl  28155  elpwiuncl  28156  elpwunicl  28168  crefi  28674  dispcmp  28686  pcmplfin  28687  indval  28835  isrnsigaOLD  28934  sigaclci  28954  sigainb  28958  elsigagen2  28970  sigapildsys  28984  ldgenpisyslem1  28985  rossros  29002  measvunilem  29034  measdivcstOLD  29046  ddeval1  29057  ddeval0  29058  omsfval  29118  omsfvalOLD  29122  omssubaddlem  29127  omssubadd  29128  omssubaddlemOLD  29131  omssubaddOLD  29132  elcarsg  29137  limsucncmpi  31105  topdifinffinlem  31750  ismrcd1  35540  elpwgded  36931  snelpwrVD  37227  elpwgdedVD  37314  sspwimpcf  37317  sspwimpcfVD  37318  sspwimpALT2  37325  pwpwuni  37397  elpwd  37412  wessf1ornlem  37459  dvnprodlem1  37821  dvnprodlem2  37822  stoweidlem50  37911  stoweidlem57  37918  pwsal  38176  saliuncl  38183  salexct  38193  fsumlesge0  38219  sge0f1o  38224  meadjuni  38295  psmeasurelem  38308  omessle  38319  caragensplit  38321  caragenelss  38322  omecl  38324  omeunile  38326  caragenuncl  38334  caragendifcl  38335  omeunle  38337  omeiunlempt  38341  carageniuncllem2  38343  carageniuncl  38344  0ome  38350  caragencmpl  38356  ovnval2  38367  ovncvrrp  38386  ovncl  38389  ovncvr2  38433  hspmbl  38451  elpwdifsn  38990  gsumlsscl  40221  lincfsuppcl  40259  linccl  40260  lincdifsn  40270  lincellss  40272  ellcoellss  40281  lindslinindsimp1  40303  lindslinindimp2lem4  40307  lindslinindsimp2lem5  40308  lindslinindsimp2  40309  lincresunit3lem2  40326  lincresunit3  40327