Theorem selpw 3864

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

Syntax hints:   <-> wb 184   e. wcel 1761   C_ wss 3325   ~Pcpw 3857

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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-ss 3339  df-pw 3859

This theorem is referenced by:  elpwg  3865  pwss  3872  snsspw  4041  pwpr  4084  pwtp  4085  pwv  4087  sspwuni  4253  iinpw  4256  iunpwss  4257  pwuni  4520  ssextss  4543  pwin  4621  pwunss  4622  xpsspw  4949  sorpsscmpl  6370  iunpw  6389  ordpwsuc  6425  fabexg  6532  abexssex  6558  qsss  7157  mapval2  7238  pmsspw  7243  uniixp  7282  fineqvlem  7523  fival  7658  hartogslem1  7752  tskwe  8116  cfval2  8425  cflim3  8427  cflim2  8428  cfslb  8431  compsscnvlem  8535  fin1a2lem13  8577  axdc3lem  8615  fpwwe2lem1  8794  fpwwe2lem11  8803  fpwwe2lem12  8804  fpwwe  8809  canthwe  8814  axgroth5  8987  axgroth6  8991  wuncn  9333  vdwmc  14035  ramub2  14071  ram0  14079  restsspw  14366  ismred  14536  mremre  14538  mreacs  14592  acsfn  14593  submacs  15488  subgacs  15709  nsgacs  15710  sylow2alem2  16110  sylow2a  16111  sylow3lem3  16121  sylow3lem6  16124  dprdres  16515  subgdmdprd  16521  pgpfac1lem5  16570  subrgmre  16869  subsubrg2  16872  lssintcl  17023  lssmre  17025  lssacs  17026  cssmre  18077  istopon  18489  isbasis2g  18512  tgval2  18520  distop  18559  cldss2  18593  ntreq0  18640  discld  18652  toponmre  18656  neisspw  18670  restdis  18741  cnntr  18838  isnrm2  18921  cmpcovf  18953  fincmp  18955  cmpsublem  18961  cmpsub  18962  cmpcld  18964  cmpfi  18970  is1stc2  19005  2ndcdisj  19019  llyi  19037  nllyi  19038  nlly2i  19039  llynlly  19040  subislly  19044  restnlly  19045  llyrest  19048  llyidm  19051  nllyidm  19052  ptuni2  19108  prdstopn  19160  qtoptop2  19231  qtopuni  19234  tgqtop  19244  isfbas2  19367  isfild  19390  elfg  19403  cfinfil  19425  csdfil  19426  supfil  19427  isufil2  19440  filssufilg  19443  uffix  19453  ufildr  19463  fin1aufil  19464  alexsubb  19577  alexsubALTlem1  19578  alexsubALT  19582  ptcmplem5  19587  cldsubg  19640  ustfn  19735  ustfilxp  19746  ustn0  19754  dscopn  20125  voliunlem2  20991  vitali  21052  shex  24549  dfch2  24745  fpwrelmap  25968  ishashinf  26018  xrsclat  26074  sigaex  26488  sigaval  26489  insiga  26516  measdivcst  26575  ballotlem2  26801  erdszelem7  27015  erdsze2lem2  27022  rellyscon  27070  dffr5  27492  islocfin  28493  neibastop2lem  28506  neibastop3  28508  topmeet  28510  topjoin  28511  neifg  28517  heibor1lem  28633  ismrcd1  28959  pw2f1ocnv  29311  filnm  29368  hbtlem6  29410  sdrgacs  29483  bj-snglss  32193  psubspset  33110  psubclsetN  33302  lcdlss  34986