Theorem elpwg 4166

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

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   C_ wss 3574   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  elpwd  4167  elpwi  4168  elpwb  4169  pwidg  4173  elpwunsn  4224  elpwdifsn  4319  prsspwg  4355  sselpwd  4807  elpw2g  4827  pwel  4920  f1opw2  6888  eldifpw  6976  elpwun  6977  elpmg  7873  fopwdom  8068  elfpw  8268  f1opwfi  8270  rankwflemb  8656  r1elwf  8659  r1pw  8708  ackbij1lem3  9044  ackbij1lem6  9047  ackbij1lem11  9052  lcmfval  15334  lcmf0val  15335  acsfn  16320  evls1val  19685  evls1rhm  19687  evls1sca  19688  fiinopn  20706  clsval2  20854  ssntr  20862  neipeltop  20933  nrmsep3  21159  cnrmi  21164  cmpcov  21192  cmpsublem  21202  conncompss  21236  kgeni  21340  tgqtop  21515  filss  21657  ufileu  21723  filufint  21724  elutop  22037  ustuqtop0  22044  metustss  22356  psmetutop  22372  axtgcont1  25367  elpwincl1  29357  elpwdifcl  29358  elpwiuncl  29359  elpwunicl  29371  dispcmp  29926  pcmplfin  29927  indval  30075  isrnsigaOLD  30175  sigaclci  30195  sigainb  30199  elsigagen2  30211  sigapildsys  30225  ldgenpisyslem1  30226  rossros  30243  measvunilem  30275  measdivcstOLD  30287  ddeval1  30297  ddeval0  30298  omsfval  30356  omssubaddlem  30361  omssubadd  30362  elcarsg  30367  limsucncmpi  32444  topdifinffinlem  33195  ismrcd1  37261  elpwgded  38780  snelpwrVD  39066  elpwgdedVD  39153  sspwimpcf  39156  sspwimpcfVD  39157  sspwimpALT2  39164  pwpwuni  39225  wessf1ornlem  39371  dvnprodlem1  40161  dvnprodlem2  40162  ovolsplit  40205  stoweidlem50  40267  stoweidlem57  40274  pwsal  40535  saliuncl  40542  salexct  40552  fsumlesge0  40594  sge0f1o  40599  meadjuni  40674  psmeasurelem  40687  omessle  40712  caragensplit  40714  caragenelss  40715  omecl  40717  omeunile  40719  caragenuncl  40727  caragendifcl  40728  omeunle  40730  omeiunlempt  40734  carageniuncllem2  40736  carageniuncl  40737  0ome  40743  caragencmpl  40749  ovnval2  40759  ovncvrrp  40778  ovncl  40781  ovncvr2  40825  hspmbl  40843  isvonmbl  40852  smfresal  40995  gsumlsscl  42164  lincfsuppcl  42202  linccl  42203  lincdifsn  42213  lincellss  42215  ellcoellss  42224  lindslinindsimp1  42246  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lincresunit3lem2  42269  lincresunit3  42270