Theorem selpw 3870

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

Syntax hints:   <-> wb 184   e. wcel 1756   C_ wss 3331   ~Pcpw 3863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338  df-ss 3345  df-pw 3865

This theorem is referenced by:  elpwg  3871  pwss  3878  snsspw  4047  pwpr  4090  pwtp  4091  pwv  4093  sspwuni  4259  iinpw  4262  iunpwss  4263  pwuni  4526  ssextss  4549  pwin  4628  pwunss  4629  xpsspw  4956  sorpsscmpl  6374  iunpw  6393  ordpwsuc  6429  fabexg  6536  abexssex  6562  qsss  7164  mapval2  7245  pmsspw  7250  uniixp  7289  fineqvlem  7530  fival  7665  hartogslem1  7759  tskwe  8123  cfval2  8432  cflim3  8434  cflim2  8435  cfslb  8438  compsscnvlem  8542  fin1a2lem13  8584  axdc3lem  8622  fpwwe2lem1  8801  fpwwe2lem11  8810  fpwwe2lem12  8811  fpwwe  8816  canthwe  8821  axgroth5  8994  axgroth6  8998  wuncn  9340  vdwmc  14042  ramub2  14078  ram0  14086  restsspw  14373  ismred  14543  mremre  14545  mreacs  14599  acsfn  14600  submacs  15496  subgacs  15719  nsgacs  15720  sylow2alem2  16120  sylow2a  16121  sylow3lem3  16131  sylow3lem6  16134  dprdres  16528  subgdmdprd  16534  pgpfac1lem5  16583  subrgmre  16892  subsubrg2  16895  lssintcl  17048  lssmre  17050  lssacs  17051  cssmre  18121  istopon  18533  isbasis2g  18556  tgval2  18564  distop  18603  cldss2  18637  ntreq0  18684  discld  18696  toponmre  18700  neisspw  18714  restdis  18785  cnntr  18882  isnrm2  18965  cmpcovf  18997  fincmp  18999  cmpsublem  19005  cmpsub  19006  cmpcld  19008  cmpfi  19014  is1stc2  19049  2ndcdisj  19063  llyi  19081  nllyi  19082  nlly2i  19083  llynlly  19084  subislly  19088  restnlly  19089  llyrest  19092  llyidm  19095  nllyidm  19096  ptuni2  19152  prdstopn  19204  qtoptop2  19275  qtopuni  19278  tgqtop  19288  isfbas2  19411  isfild  19434  elfg  19447  cfinfil  19469  csdfil  19470  supfil  19471  isufil2  19484  filssufilg  19487  uffix  19497  ufildr  19507  fin1aufil  19508  alexsubb  19621  alexsubALTlem1  19622  alexsubALT  19626  ptcmplem5  19631  cldsubg  19684  ustfn  19779  ustfilxp  19790  ustn0  19798  dscopn  20169  voliunlem2  21035  vitali  21096  shex  24617  dfch2  24813  fpwrelmap  26036  ishashinf  26088  xrsclat  26144  sigaex  26555  sigaval  26556  insiga  26583  measdivcst  26642  ballotlem2  26874  erdszelem7  27088  erdsze2lem2  27095  rellyscon  27143  dffr5  27566  islocfin  28571  neibastop2lem  28584  neibastop3  28586  topmeet  28588  topjoin  28589  neifg  28595  heibor1lem  28711  ismrcd1  29037  pw2f1ocnv  29389  filnm  29446  hbtlem6  29488  sdrgacs  29561  bj-snglss  32466  psubspset  33391  psubclsetN  33583  lcdlss  35267