Theorem selpw 3931

Description: Setvar variable membership in a power class (common case). See elpw 3930. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
selpw	|- ( x e. ~P A <-> x C_ A )

Distinct variable group:   x, A

Proof of Theorem selpw

Step	Hyp	Ref	Expression
1		vex 3025	. 2 |- x e. _V
2	1	elpw 3930	1 |- ( x e. ~P A <-> x C_ A )

Syntax hints:   <-> wb 187   e. wcel 1872   C_ wss 3379   ~Pcpw 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386  df-ss 3393  df-pw 3926

This theorem is referenced by:  elpwg  3932  pwss  3939  snsspw  4114  pwpr  4158  pwtp  4159  pwv  4161  sspwuni  4331  iinpw  4334  iunpwss  4335  pwuni  4595  ssextss  4618  pwin  4700  pwunss  4701  sorpsscmpl  6540  iunpw  6563  ordpwsuc  6600  fabexg  6707  abexssex  6733  qsss  7379  mapval2  7456  pmsspw  7461  uniixp  7500  fineqvlem  7739  fival  7879  hartogslem1  8010  tskwe  8336  cfval2  8641  cflim3  8643  cflim2  8644  cfslb  8647  compsscnvlem  8751  fin1a2lem13  8793  axdc3lem  8831  fpwwe2lem1  9007  fpwwe2lem11  9016  fpwwe2lem12  9017  fpwwe  9022  canthwe  9027  axgroth5  9200  axgroth6  9204  wuncn  9545  ishashinf  12574  vdwmc  14871  ramub2  14914  ram0  14923  restsspw  15273  ismred  15451  mremre  15453  mreacs  15507  acsfn  15508  submacs  16555  subgacs  16795  nsgacs  16796  sylow2alem2  17213  sylow2a  17214  sylow3lem3  17224  sylow3lem6  17227  dprdres  17604  subgdmdprd  17610  pgpfac1lem5  17655  subrgmre  17975  subsubrg2  17978  lssintcl  18130  lssmre  18132  lssacs  18133  cssmre  19198  istopon  19882  isbasis2g  19905  tgval2  19913  unitg  19924  distop  19953  cldss2  19987  ntreq0  20035  discld  20047  toponmre  20051  neisspw  20065  restdis  20136  cnntr  20233  isnrm2  20316  cmpcovf  20348  fincmp  20350  cmpsublem  20356  cmpsub  20357  cmpcld  20359  cmpfi  20365  is1stc2  20399  2ndcdisj  20413  llyi  20431  nllyi  20432  nlly2i  20433  llynlly  20434  subislly  20438  restnlly  20439  llyrest  20442  llyidm  20445  nllyidm  20446  islocfin  20474  ptuni2  20533  prdstopn  20585  qtoptop2  20656  qtopuni  20659  tgqtop  20669  isfbas2  20792  isfild  20815  elfg  20828  cfinfil  20850  csdfil  20851  supfil  20852  isufil2  20865  filssufilg  20868  uffix  20878  ufildr  20888  fin1aufil  20889  alexsubb  21003  alexsubALTlem1  21004  alexsubALT  21008  ptcmplem5  21013  cldsubg  21067  ustfn  21158  ustfilxp  21169  ustn0  21177  dscopn  21530  voliunlem2  22446  vitali  22513  shex  26807  dfch2  27002  fpwrelmap  28268  xrsclat  28393  cmpcref  28629  sigaex  28883  sigaval  28884  insiga  28911  sigapisys  28929  sigaldsys  28933  measdivcst  28999  ballotlem2  29273  erdszelem7  29872  erdsze2lem2  29879  rellyscon  29926  dffr5  30344  neibastop2lem  30965  neibastop3  30967  topmeet  30969  topjoin  30970  neifg  30976  bj-snglss  31475  dissneqlem  31649  topdifinfeq  31660  heibor1lem  32048  psubspset  33221  psubclsetN  33413  lcdlss  35099  ismrcd1  35452  pw2f1ocnv  35805  filnm  35861  hbtlem6  35901  sdrgacs  35980  elmapintrab  36095  clcnvlem  36143  psshepw  36297  nbuhgr  39147  nbuhgr2vtx1edgblem  39155  submgmacs  39395