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

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

Proof of Theorem selpw
StepHypRef Expression
1 vex 3175 . 2 𝑥 ∈ V
21elpw 4113 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1976  wss 3539  𝒫 cpw 4107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-pw 4109
This theorem is referenced by:  elpwg  4115  pwss  4122  snsspw  4310  pwpr  4362  pwtp  4363  pwv  4365  sspwuni  4541  iinpw  4544  iunpwss  4545  pwuni  4820  ssextss  4843  pwin  4932  pwunss  4933  sorpsscmpl  6823  iunpw  6847  ordpwsuc  6884  fabexg  6992  abexssex  7018  qsss  7672  mapval2  7750  pmsspw  7755  uniixp  7794  fineqvlem  8036  fival  8178  hartogslem1  8307  tskwe  8636  cfval2  8942  cflim3  8944  cflim2  8945  cfslb  8948  compsscnvlem  9052  fin1a2lem13  9094  axdc3lem  9132  fpwwe2lem1  9309  fpwwe2lem11  9318  fpwwe2lem12  9319  fpwwe  9324  canthwe  9329  axgroth5  9502  axgroth6  9506  wuncn  9847  ishashinf  13056  vdwmc  15466  ramub2  15502  ram0  15510  restsspw  15861  ismred  16031  mremre  16033  mreacs  16088  acsfn  16089  submacs  17134  subgacs  17398  nsgacs  17399  sylow2alem2  17802  sylow2a  17803  sylow3lem3  17813  sylow3lem6  17816  dprdres  18196  subgdmdprd  18202  pgpfac1lem5  18247  subrgmre  18573  subsubrg2  18576  lssintcl  18731  lssmre  18733  lssacs  18734  cssmre  19798  istopon  20482  isbasis2g  20505  tgval2  20513  unitg  20524  distop  20552  cldss2  20586  ntreq0  20633  discld  20645  toponmre  20649  neisspw  20663  restdis  20734  cnntr  20831  isnrm2  20914  cmpcovf  20946  fincmp  20948  cmpsublem  20954  cmpsub  20955  cmpcld  20957  cmpfi  20963  is1stc2  20997  2ndcdisj  21011  llyi  21029  nllyi  21030  nlly2i  21031  llynlly  21032  subislly  21036  restnlly  21037  llyrest  21040  llyidm  21043  nllyidm  21044  islocfin  21072  ptuni2  21131  prdstopn  21183  qtoptop2  21254  qtopuni  21257  tgqtop  21267  isfbas2  21391  isfild  21414  elfg  21427  cfinfil  21449  csdfil  21450  supfil  21451  isufil2  21464  filssufilg  21467  uffix  21477  ufildr  21487  fin1aufil  21488  alexsubb  21602  alexsubALTlem1  21603  alexsubALT  21607  ptcmplem5  21612  cldsubg  21666  ustfn  21757  ustfilxp  21768  ustn0  21776  dscopn  22129  voliunlem2  23043  vitali  23105  shex  27259  dfch2  27456  fpwrelmap  28702  xrsclat  28817  cmpcref  29051  sigaex  29305  sigaval  29306  insiga  29333  sigapisys  29351  sigaldsys  29355  measdivcst  29421  ballotlem2  29683  erdszelem7  30239  erdsze2lem2  30246  rellyscon  30293  dffr5  30702  neibastop2lem  31331  neibastop3  31333  topmeet  31335  topjoin  31336  neifg  31342  bj-snglss  31947  bj-restpw  32022  dissneqlem  32159  topdifinfeq  32170  heibor1lem  32574  psubspset  33844  psubclsetN  34036  lcdlss  35722  ismrcd1  36075  pw2f1ocnv  36418  filnm  36474  hbtlem6  36514  sdrgacs  36586  elmapintrab  36697  clcnvlem  36745  psshepw  36898  nbuhgr  40560  nbuhgr2vtx1edgblem  40568  submgmacs  41589
  Copyright terms: Public domain W3C validator