Theorem selpw 3456

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

Syntax hints:   <-> wb 104   e. wcel 1445   C_ wss 3013   ~Pcpw 3449

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-in 3019  df-ss 3026  df-pw 3451

This theorem is referenced by:  ordpwsucss  4411  fabexg  5233  abexssex  5934  qsss  6391  mapval2  6475  pmsspw  6480  uniixp  6518  exmidpw  6704  npsspw  7127  restsspw  11830  istopon  11880  isbasis2g  11911  tgval2  11919  unitg  11930  distop  11953  cldss2  11974  ntreq0  12000  discld  12004  neisspw  12016  restdis  12052  cnntr  12092