Theorem selpw 3970

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

Syntax hints:   <-> wb 189   e. wcel 1898   C_ wss 3416   ~Pcpw 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-pw 3965

This theorem is referenced by:  elpwg  3971  pwss  3978  snsspw  4156  pwpr  4208  pwtp  4209  pwv  4211  sspwuni  4381  iinpw  4384  iunpwss  4385  pwuni  4645  ssextss  4668  pwin  4757  pwunss  4758  sorpsscmpl  6609  iunpw  6632  ordpwsuc  6669  fabexg  6776  abexssex  6802  qsss  7450  mapval2  7527  pmsspw  7532  uniixp  7571  fineqvlem  7812  fival  7952  hartogslem1  8083  tskwe  8410  cfval2  8716  cflim3  8718  cflim2  8719  cfslb  8722  compsscnvlem  8826  fin1a2lem13  8868  axdc3lem  8906  fpwwe2lem1  9082  fpwwe2lem11  9091  fpwwe2lem12  9092  fpwwe  9097  canthwe  9102  axgroth5  9275  axgroth6  9279  wuncn  9620  ishashinf  12659  vdwmc  14977  ramub2  15020  ram0  15029  restsspw  15379  ismred  15557  mremre  15559  mreacs  15613  acsfn  15614  submacs  16661  subgacs  16901  nsgacs  16902  sylow2alem2  17319  sylow2a  17320  sylow3lem3  17330  sylow3lem6  17333  dprdres  17710  subgdmdprd  17716  pgpfac1lem5  17761  subrgmre  18081  subsubrg2  18084  lssintcl  18236  lssmre  18238  lssacs  18239  cssmre  19305  istopon  19989  isbasis2g  20012  tgval2  20020  unitg  20031  distop  20060  cldss2  20094  ntreq0  20142  discld  20154  toponmre  20158  neisspw  20172  restdis  20243  cnntr  20340  isnrm2  20423  cmpcovf  20455  fincmp  20457  cmpsublem  20463  cmpsub  20464  cmpcld  20466  cmpfi  20472  is1stc2  20506  2ndcdisj  20520  llyi  20538  nllyi  20539  nlly2i  20540  llynlly  20541  subislly  20545  restnlly  20546  llyrest  20549  llyidm  20552  nllyidm  20553  islocfin  20581  ptuni2  20640  prdstopn  20692  qtoptop2  20763  qtopuni  20766  tgqtop  20776  isfbas2  20899  isfild  20922  elfg  20935  cfinfil  20957  csdfil  20958  supfil  20959  isufil2  20972  filssufilg  20975  uffix  20985  ufildr  20995  fin1aufil  20996  alexsubb  21110  alexsubALTlem1  21111  alexsubALT  21115  ptcmplem5  21120  cldsubg  21174  ustfn  21265  ustfilxp  21276  ustn0  21284  dscopn  21637  voliunlem2  22553  vitali  22620  shex  26914  dfch2  27109  fpwrelmap  28367  xrsclat  28491  cmpcref  28726  sigaex  28980  sigaval  28981  insiga  29008  sigapisys  29026  sigaldsys  29030  measdivcst  29096  ballotlem2  29370  erdszelem7  29969  erdsze2lem2  29976  rellyscon  30023  dffr5  30442  neibastop2lem  31065  neibastop3  31067  topmeet  31069  topjoin  31070  neifg  31076  bj-snglss  31609  dissneqlem  31787  topdifinfeq  31798  heibor1lem  32186  psubspset  33354  psubclsetN  33546  lcdlss  35232  ismrcd1  35585  pw2f1ocnv  35937  filnm  35993  hbtlem6  36033  sdrgacs  36112  elmapintrab  36227  clcnvlem  36275  psshepw  36429  nbuhgr  39461  nbuhgr2vtx1edgblem  39469  submgmacs  40077