Theorem selpw 4010

Description: Setvar variable membership in a power class (common case). See elpw 4009. (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 3109	. 2 |- x e. _V
2	1	elpw 4009	1 |- ( x e. ~P A <-> x C_ A )

Syntax hints:   <-> wb 184   e. wcel 1762   C_ wss 3469   ~Pcpw 4003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483  df-pw 4005

This theorem is referenced by:  elpwg  4011  pwss  4018  snsspw  4191  pwpr  4234  pwtp  4235  pwv  4237  sspwuni  4404  iinpw  4407  iunpwss  4408  pwuni  4671  ssextss  4694  pwin  4777  pwunss  4778  xpsspw  5107  sorpsscmpl  6566  iunpw  6585  ordpwsuc  6621  fabexg  6730  abexssex  6756  qsss  7362  mapval2  7438  pmsspw  7443  uniixp  7482  fineqvlem  7724  fival  7861  hartogslem1  7956  tskwe  8320  cfval2  8629  cflim3  8631  cflim2  8632  cfslb  8635  compsscnvlem  8739  fin1a2lem13  8781  axdc3lem  8819  fpwwe2lem1  8998  fpwwe2lem11  9007  fpwwe2lem12  9008  fpwwe  9013  canthwe  9018  axgroth5  9191  axgroth6  9195  wuncn  9536  vdwmc  14344  ramub2  14380  ram0  14388  restsspw  14676  ismred  14846  mremre  14848  mreacs  14902  acsfn  14903  submacs  15799  subgacs  16024  nsgacs  16025  sylow2alem2  16427  sylow2a  16428  sylow3lem3  16438  sylow3lem6  16441  dprdres  16858  subgdmdprd  16864  pgpfac1lem5  16913  subrgmre  17229  subsubrg2  17232  lssintcl  17386  lssmre  17388  lssacs  17389  cssmre  18484  istopon  19186  isbasis2g  19209  tgval2  19217  distop  19256  cldss2  19290  ntreq0  19337  discld  19349  toponmre  19353  neisspw  19367  restdis  19438  cnntr  19535  isnrm2  19618  cmpcovf  19650  fincmp  19652  cmpsublem  19658  cmpsub  19659  cmpcld  19661  cmpfi  19667  is1stc2  19702  2ndcdisj  19716  llyi  19734  nllyi  19735  nlly2i  19736  llynlly  19737  subislly  19741  restnlly  19742  llyrest  19745  llyidm  19748  nllyidm  19749  ptuni2  19805  prdstopn  19857  qtoptop2  19928  qtopuni  19931  tgqtop  19941  isfbas2  20064  isfild  20087  elfg  20100  cfinfil  20122  csdfil  20123  supfil  20124  isufil2  20137  filssufilg  20140  uffix  20150  ufildr  20160  fin1aufil  20161  alexsubb  20274  alexsubALTlem1  20275  alexsubALT  20279  ptcmplem5  20284  cldsubg  20337  ustfn  20432  ustfilxp  20443  ustn0  20451  dscopn  20822  voliunlem2  21689  vitali  21750  shex  25791  dfch2  25987  fpwrelmap  27214  ishashinf  27260  xrsclat  27316  sigaex  27735  sigaval  27736  insiga  27763  measdivcst  27822  ballotlem2  28053  erdszelem7  28267  erdsze2lem2  28274  rellyscon  28322  dffr5  28745  islocfin  29755  neibastop2lem  29768  neibastop3  29770  topmeet  29772  topjoin  29773  neifg  29779  heibor1lem  29895  ismrcd1  30221  pw2f1ocnv  30572  filnm  30629  hbtlem6  30671  sdrgacs  30744  bj-snglss  33484  psubspset  34415  psubclsetN  34607  lcdlss  36291