Theorem elpwg 3987

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

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1868   C_ wss 3436   ~Pcpw 3979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-in 3443  df-ss 3450  df-pw 3981

This theorem is referenced by:  elpwi  3988  pwidg  3992  elpwunsn  4037  prsspwg  4154  elpw2g  4583  pwel  4669  f1opw2  6532  eldifpw  6613  elpwun  6614  elpmg  7491  fopwdom  7682  elfpw  7878  f1opwfi  7880  rankwflemb  8265  r1elwf  8268  r1pw  8317  ackbij1lem3  8652  ackbij1lem6  8655  ackbij1lem11  8660  lcmfval  14578  lcmf0val  14579  lcmfvalOLD  14582  mreexexlemd  15537  acsfn  15552  evls1val  18896  evls1rhm  18898  evls1sca  18899  fiinopn  19917  clsval2  20051  ssntr  20059  neipeltop  20131  nrmsep3  20357  cnrmi  20362  cmpcov  20390  cmpsublem  20400  concompss  20434  kgeni  20538  tgqtop  20713  filss  20854  ufileu  20920  filufint  20921  ustssel  21206  elutop  21234  ustuqtop0  21241  metustss  21552  psmetutop  21568  axtgcont1  24502  issubgo  26016  sselpwd  28141  elpwincl1  28142  elpwdifcl  28143  elpwiuncl  28144  elpwunicl  28157  crefi  28669  dispcmp  28681  pcmplfin  28682  indval  28830  isrnsigaOLD  28929  sigaclci  28949  sigainb  28953  elsigagen2  28965  sigapildsys  28979  ldgenpisyslem1  28980  rossros  28997  measvunilem  29029  measdivcstOLD  29041  ddeval1  29052  ddeval0  29053  omsfval  29113  omsfvalOLD  29117  omssubaddlem  29122  omssubadd  29123  omssubaddlemOLD  29126  omssubaddOLD  29127  elcarsg  29132  limsucncmpi  31097  topdifinffinlem  31690  ismrcd1  35458  elpwgded  36788  snelpwrVD  37087  elpwgdedVD  37174  sspwimpcf  37177  sspwimpcfVD  37178  sspwimpALT2  37185  pwpwuni  37258  elpwd  37275  wessf1ornlem  37308  dvnprodlem1  37640  dvnprodlem2  37641  stoweidlem50  37730  stoweidlem57  37737  pwsal  37976  saliuncl  37983  fsumlesge0  38006  sge0f1o  38011  meadjuni  38073  psmeasurelem  38086  omessle  38097  caragensplit  38099  caragenelss  38100  omecl  38102  omeunile  38104  caragenuncl  38112  caragendifcl  38113  omeunle  38115  omeiunlempt  38119  carageniuncllem2  38121  carageniuncl  38122  0ome  38128  ovnval2  38141  ovncvrrp  38160  ovncl  38163  elpwdifsn  38694  gsumlsscl  39441  lincfsuppcl  39479  linccl  39480  lincdifsn  39490  lincellss  39492  ellcoellss  39501  lindslinindsimp1  39523  lindslinindimp2lem4  39527  lindslinindsimp2lem5  39528  lindslinindsimp2  39529  lincresunit3lem2  39546  lincresunit3  39547