Theorem selpw 4022

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

Syntax hints:   <-> wb 184   e. wcel 1819   C_ wss 3471   ~Pcpw 4015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485  df-pw 4017

This theorem is referenced by:  elpwg  4023  pwss  4030  snsspw  4203  pwpr  4247  pwtp  4248  pwv  4250  sspwuni  4421  iinpw  4424  iunpwss  4425  pwuni  4687  ssextss  4710  pwin  4793  pwunss  4794  xpsspw  5125  sorpsscmpl  6590  iunpw  6613  ordpwsuc  6649  fabexg  6755  abexssex  6781  qsss  7390  mapval2  7467  pmsspw  7472  uniixp  7511  fineqvlem  7753  fival  7890  hartogslem1  7985  tskwe  8348  cfval2  8657  cflim3  8659  cflim2  8660  cfslb  8663  compsscnvlem  8767  fin1a2lem13  8809  axdc3lem  8847  fpwwe2lem1  9026  fpwwe2lem11  9035  fpwwe2lem12  9036  fpwwe  9041  canthwe  9046  axgroth5  9219  axgroth6  9223  wuncn  9564  vdwmc  14508  ramub2  14544  ram0  14552  restsspw  14849  ismred  15019  mremre  15021  mreacs  15075  acsfn  15076  submacs  16123  subgacs  16363  nsgacs  16364  sylow2alem2  16765  sylow2a  16766  sylow3lem3  16776  sylow3lem6  16779  dprdres  17202  subgdmdprd  17208  pgpfac1lem5  17257  subrgmre  17580  subsubrg2  17583  lssintcl  17737  lssmre  17739  lssacs  17740  cssmre  18851  istopon  19553  isbasis2g  19576  tgval2  19584  unitg  19595  distop  19624  cldss2  19658  ntreq0  19705  discld  19717  toponmre  19721  neisspw  19735  restdis  19806  cnntr  19903  isnrm2  19986  cmpcovf  20018  fincmp  20020  cmpsublem  20026  cmpsub  20027  cmpcld  20029  cmpfi  20035  is1stc2  20069  2ndcdisj  20083  llyi  20101  nllyi  20102  nlly2i  20103  llynlly  20104  subislly  20108  restnlly  20109  llyrest  20112  llyidm  20115  nllyidm  20116  islocfin  20144  ptuni2  20203  prdstopn  20255  qtoptop2  20326  qtopuni  20329  tgqtop  20339  isfbas2  20462  isfild  20485  elfg  20498  cfinfil  20520  csdfil  20521  supfil  20522  isufil2  20535  filssufilg  20538  uffix  20548  ufildr  20558  fin1aufil  20559  alexsubb  20672  alexsubALTlem1  20673  alexsubALT  20677  ptcmplem5  20682  cldsubg  20735  ustfn  20830  ustfilxp  20841  ustn0  20849  dscopn  21220  voliunlem2  22087  vitali  22148  shex  26256  dfch2  26452  fpwrelmap  27713  ishashinf  27766  xrsclat  27828  cmpcref  28014  sigaex  28282  sigaval  28283  insiga  28310  measdivcst  28369  ballotlem2  28624  erdszelem7  28838  erdsze2lem2  28845  rellyscon  28893  dffr5  29400  neibastop2lem  30383  neibastop3  30385  topmeet  30387  topjoin  30388  neifg  30394  heibor1lem  30510  ismrcd1  30835  pw2f1ocnv  31183  filnm  31240  hbtlem6  31282  sdrgacs  31354  submgmacs  32754  bj-snglss  34671  psubspset  35611  psubclsetN  35803  lcdlss  37489