Theorem selpw 4165

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

Syntax hints:   <-> wb 196   e. wcel 1990   C_ wss 3574   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  elpwg  4166  pwss  4175  snsspw  4375  pwpr  4430  pwtp  4431  pwv  4433  pwuni  4474  sspwuni  4611  iinpw  4617  iunpwss  4618  ssextss  4922  pwin  5018  pwunss  5019  sorpsscmpl  6948  iunpw  6978  ordpwsuc  7015  fabexg  7122  abexssex  7149  qsss  7808  mapval2  7887  pmsspw  7892  uniixp  7931  fineqvlem  8174  fival  8318  hartogslem1  8447  tskwe  8776  cfval2  9082  cflim3  9084  cflim2  9085  cfslb  9088  compsscnvlem  9192  fin1a2lem13  9234  axdc3lem  9272  fpwwe2lem1  9453  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe  9468  canthwe  9473  axgroth5  9646  axgroth6  9650  wuncn  9991  ishashinf  13247  vdwmc  15682  ramub2  15718  ram0  15726  restsspw  16092  ismred  16262  mremre  16264  mreacs  16319  acsfn  16320  submacs  17365  subgacs  17629  nsgacs  17630  sylow2alem2  18033  sylow2a  18034  sylow3lem3  18044  sylow3lem6  18047  dprdres  18427  subgdmdprd  18433  pgpfac1lem5  18478  subrgmre  18804  subsubrg2  18807  lssintcl  18964  lssmre  18966  lssacs  18967  cssmre  20037  istopon  20717  isbasis2g  20752  tgval2  20760  unitg  20771  distop  20799  cldss2  20834  ntreq0  20881  discld  20893  toponmre  20897  neisspw  20911  restdis  20982  cnntr  21079  isnrm2  21162  cmpcovf  21194  fincmp  21196  cmpsublem  21202  cmpsub  21203  cmpcld  21205  cmpfi  21211  is1stc2  21245  2ndcdisj  21259  llyi  21277  nllyi  21278  nlly2i  21279  llynlly  21280  subislly  21284  restnlly  21285  llyrest  21288  llyidm  21291  nllyidm  21292  islocfin  21320  ptuni2  21379  prdstopn  21431  qtoptop2  21502  qtopuni  21505  tgqtop  21515  isfbas2  21639  isfild  21662  elfg  21675  cfinfil  21697  csdfil  21698  supfil  21699  isufil2  21712  filssufilg  21715  uffix  21725  ufildr  21735  fin1aufil  21736  alexsubb  21850  alexsubALTlem1  21851  alexsubALT  21855  ptcmplem5  21860  cldsubg  21914  ustfn  22005  ustfilxp  22016  ustn0  22024  dscopn  22378  voliunlem2  23319  vitali  23382  nbuhgr  26239  nbuhgr2vtx1edgblem  26247  shex  28069  dfch2  28266  fpwrelmap  29508  xrsclat  29680  cmpcref  29917  sigaex  30172  sigaval  30173  insiga  30200  sigapisys  30218  sigaldsys  30222  measdivcst  30288  ballotlem2  30550  erdszelem7  31179  erdsze2lem2  31186  rellysconn  31233  dffr5  31643  neibastop2lem  32355  neibastop3  32357  topmeet  32359  topjoin  32360  neifg  32366  bj-snglss  32958  bj-restpw  33045  bj-ismooredr2  33065  dissneqlem  33187  topdifinfeq  33198  heibor1lem  33608  psubspset  35030  psubclsetN  35222  lcdlss  36908  ismrcd1  37261  pw2f1ocnv  37604  filnm  37660  hbtlem6  37699  sdrgacs  37771  elmapintrab  37882  clcnvlem  37930  psshepw  38082  sprsymrelfo  41747  uspgrsprfo  41756  submgmacs  41804  setrec2fun  42439