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

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

Proof of Theorem selpw
StepHypRef Expression
1 vex 3394 . 2 𝑥 ∈ V
21elpw 4357 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2156  wss 3769  𝒫 cpw 4351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783  df-pw 4353
This theorem is referenced by:  elpwg  4359  pwss  4368  snsspw  4563  pwpr  4624  pwtp  4625  pwv  4627  pwuni  4668  sspwuni  4803  iinpw  4809  iunpwss  4810  ssextss  5112  pwin  5213  pwunss  5214  sorpsscmpl  7178  iunpw  7208  ordpwsuc  7245  fabexg  7352  abexssex  7379  qsss  8043  mapval2  8122  pmsspw  8127  uniixp  8168  fineqvlem  8413  fival  8557  hartogslem1  8686  tskwe  9059  cfval2  9367  cflim3  9369  cflim2  9370  cfslb  9373  compsscnvlem  9477  fin1a2lem13  9519  axdc3lem  9557  fpwwe2lem1  9738  fpwwe2lem11  9747  fpwwe2lem12  9748  fpwwe  9753  canthwe  9758  axgroth5  9931  axgroth6  9935  wuncn  10276  ishashinf  13464  vdwmc  15899  ramub2  15935  ram0  15943  restsspw  16297  ismred  16467  mremre  16469  mreacs  16523  acsfn  16524  submacs  17570  subgacs  17831  nsgacs  17832  sylow2alem2  18234  sylow2a  18235  sylow3lem3  18245  sylow3lem6  18248  dprdres  18629  subgdmdprd  18635  pgpfac1lem5  18680  subrgmre  19008  subsubrg2  19011  lssintcl  19171  lssmre  19173  lssacs  19174  cssmre  20247  istopon  20930  isbasis2g  20966  tgval2  20974  unitg  20985  distop  21013  cldss2  21048  ntreq0  21095  discld  21107  toponmre  21111  neisspw  21125  restdis  21196  cnntr  21293  isnrm2  21376  cmpcovf  21408  fincmp  21410  cmpsublem  21416  cmpsub  21417  cmpcld  21419  cmpfi  21425  is1stc2  21459  2ndcdisj  21473  llyi  21491  nllyi  21492  nlly2i  21493  llynlly  21494  subislly  21498  restnlly  21499  llyrest  21502  llyidm  21505  nllyidm  21506  islocfin  21534  ptuni2  21593  prdstopn  21645  qtoptop2  21716  qtopuni  21719  tgqtop  21729  isfbas2  21852  isfild  21875  elfg  21888  cfinfil  21910  csdfil  21911  supfil  21912  isufil2  21925  filssufilg  21928  uffix  21938  ufildr  21948  fin1aufil  21949  alexsubb  22063  alexsubALTlem1  22064  alexsubALT  22068  ptcmplem5  22073  cldsubg  22127  ustfn  22218  ustfilxp  22229  ustn0  22237  dscopn  22591  voliunlem2  23532  vitali  23594  nbuhgr  26455  nbuhgr2vtx1edgblem  26463  shex  28397  dfch2  28594  fpwrelmap  29835  xrsclat  30005  cmpcref  30242  sigaex  30497  sigaval  30498  insiga  30525  sigapisys  30543  sigaldsys  30547  measdivcst  30613  ballotlem2  30875  erdszelem7  31502  erdsze2lem2  31509  rellysconn  31556  dffr5  31965  neibastop2lem  32676  neibastop3  32678  topmeet  32680  topjoin  32681  neifg  32687  bj-snglss  33268  bj-restpw  33356  bj-ismooredr2  33376  dissneqlem  33504  topdifinfeq  33514  heibor1lem  33919  psubspset  35524  psubclsetN  35716  lcdlss  37400  ismrcd1  37763  pw2f1ocnv  38105  filnm  38161  hbtlem6  38200  sdrgacs  38272  elmapintrab  38382  clcnvlem  38430  psshepw  38582  sprsymrelfo  42315  uspgrsprfo  42324  submgmacs  42372  setrec2fun  43007  setrecsres  43016
  Copyright terms: Public domain W3C validator