MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  selpw Unicode version

Theorem selpw 4019
Description: Setvar variable membership in a power class (common case). See elpw 4018. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
selpw
Distinct variable group:   ,

Proof of Theorem selpw
StepHypRef Expression
1 vex 3112 . 2
21elpw 4018 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818  C_wss 3475  ~Pcpw 4012
This theorem is referenced by:  elpwg  4020  pwss  4027  snsspw  4201  pwpr  4245  pwtp  4246  pwv  4248  sspwuni  4416  iinpw  4419  iunpwss  4420  pwuni  4683  ssextss  4706  pwin  4789  pwunss  4790  xpsspw  5121  sorpsscmpl  6591  iunpw  6614  ordpwsuc  6650  fabexg  6756  abexssex  6782  qsss  7391  mapval2  7468  pmsspw  7473  uniixp  7512  fineqvlem  7754  fival  7892  hartogslem1  7988  tskwe  8352  cfval2  8661  cflim3  8663  cflim2  8664  cfslb  8667  compsscnvlem  8771  fin1a2lem13  8813  axdc3lem  8851  fpwwe2lem1  9030  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe  9045  canthwe  9050  axgroth5  9223  axgroth6  9227  wuncn  9568  vdwmc  14496  ramub2  14532  ram0  14540  restsspw  14829  ismred  14999  mremre  15001  mreacs  15055  acsfn  15056  submacs  15996  subgacs  16236  nsgacs  16237  sylow2alem2  16638  sylow2a  16639  sylow3lem3  16649  sylow3lem6  16652  dprdres  17075  subgdmdprd  17081  pgpfac1lem5  17130  subrgmre  17453  subsubrg2  17456  lssintcl  17610  lssmre  17612  lssacs  17613  cssmre  18724  istopon  19426  isbasis2g  19449  tgval2  19457  unitg  19468  distop  19497  cldss2  19531  ntreq0  19578  discld  19590  toponmre  19594  neisspw  19608  restdis  19679  cnntr  19776  isnrm2  19859  cmpcovf  19891  fincmp  19893  cmpsublem  19899  cmpsub  19900  cmpcld  19902  cmpfi  19908  is1stc2  19943  2ndcdisj  19957  llyi  19975  nllyi  19976  nlly2i  19977  llynlly  19978  subislly  19982  restnlly  19983  llyrest  19986  llyidm  19989  nllyidm  19990  islocfin  20018  ptuni2  20077  prdstopn  20129  qtoptop2  20200  qtopuni  20203  tgqtop  20213  isfbas2  20336  isfild  20359  elfg  20372  cfinfil  20394  csdfil  20395  supfil  20396  isufil2  20409  filssufilg  20412  uffix  20422  ufildr  20432  fin1aufil  20433  alexsubb  20546  alexsubALTlem1  20547  alexsubALT  20551  ptcmplem5  20556  cldsubg  20609  ustfn  20704  ustfilxp  20715  ustn0  20723  dscopn  21094  voliunlem2  21961  vitali  22022  shex  26129  dfch2  26325  fpwrelmap  27556  ishashinf  27606  xrsclat  27668  cmpcref  27853  sigaex  28109  sigaval  28110  insiga  28137  measdivcst  28196  ballotlem2  28427  erdszelem7  28641  erdsze2lem2  28648  rellyscon  28696  dffr5  29182  neibastop2lem  30178  neibastop3  30180  topmeet  30182  topjoin  30183  neifg  30189  heibor1lem  30305  ismrcd1  30630  pw2f1ocnv  30979  filnm  31036  hbtlem6  31078  sdrgacs  31150  submgmacs  32492  bj-snglss  34528  psubspset  35468  psubclsetN  35660  lcdlss  37346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator