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

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

Proof of Theorem selpw
StepHypRef Expression
1 vex 3234 . 2 𝑥 ∈ V
21elpw 4197 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 2030  wss 3607  𝒫 cpw 4191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  elpwg  4199  pwss  4208  snsspw  4407  pwpr  4462  pwtp  4463  pwv  4465  pwuni  4506  sspwuni  4643  iinpw  4649  iunpwss  4650  ssextss  4952  pwin  5047  pwunss  5048  sorpsscmpl  6990  iunpw  7020  ordpwsuc  7057  fabexg  7164  abexssex  7191  qsss  7851  mapval2  7929  pmsspw  7934  uniixp  7973  fineqvlem  8215  fival  8359  hartogslem1  8488  tskwe  8814  cfval2  9120  cflim3  9122  cflim2  9123  cfslb  9126  compsscnvlem  9230  fin1a2lem13  9272  axdc3lem  9310  fpwwe2lem1  9491  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe  9506  canthwe  9511  axgroth5  9684  axgroth6  9688  wuncn  10029  ishashinf  13285  vdwmc  15729  ramub2  15765  ram0  15773  restsspw  16139  ismred  16309  mremre  16311  mreacs  16366  acsfn  16367  submacs  17412  subgacs  17676  nsgacs  17677  sylow2alem2  18079  sylow2a  18080  sylow3lem3  18090  sylow3lem6  18093  dprdres  18473  subgdmdprd  18479  pgpfac1lem5  18524  subrgmre  18852  subsubrg2  18855  lssintcl  19012  lssmre  19014  lssacs  19015  cssmre  20085  istopon  20765  isbasis2g  20800  tgval2  20808  unitg  20819  distop  20847  cldss2  20882  ntreq0  20929  discld  20941  toponmre  20945  neisspw  20959  restdis  21030  cnntr  21127  isnrm2  21210  cmpcovf  21242  fincmp  21244  cmpsublem  21250  cmpsub  21251  cmpcld  21253  cmpfi  21259  is1stc2  21293  2ndcdisj  21307  llyi  21325  nllyi  21326  nlly2i  21327  llynlly  21328  subislly  21332  restnlly  21333  llyrest  21336  llyidm  21339  nllyidm  21340  islocfin  21368  ptuni2  21427  prdstopn  21479  qtoptop2  21550  qtopuni  21553  tgqtop  21563  isfbas2  21686  isfild  21709  elfg  21722  cfinfil  21744  csdfil  21745  supfil  21746  isufil2  21759  filssufilg  21762  uffix  21772  ufildr  21782  fin1aufil  21783  alexsubb  21897  alexsubALTlem1  21898  alexsubALT  21902  ptcmplem5  21907  cldsubg  21961  ustfn  22052  ustfilxp  22063  ustn0  22071  dscopn  22425  voliunlem2  23365  vitali  23427  nbuhgr  26284  nbuhgr2vtx1edgblem  26292  shex  28197  dfch2  28394  fpwrelmap  29636  xrsclat  29808  cmpcref  30045  sigaex  30300  sigaval  30301  insiga  30328  sigapisys  30346  sigaldsys  30350  measdivcst  30416  ballotlem2  30678  erdszelem7  31305  erdsze2lem2  31312  rellysconn  31359  dffr5  31769  neibastop2lem  32480  neibastop3  32482  topmeet  32484  topjoin  32485  neifg  32491  bj-snglss  33083  bj-restpw  33170  bj-ismooredr2  33190  dissneqlem  33317  topdifinfeq  33328  heibor1lem  33738  psubspset  35348  psubclsetN  35540  lcdlss  37225  ismrcd1  37578  pw2f1ocnv  37921  filnm  37977  hbtlem6  38016  sdrgacs  38088  elmapintrab  38199  clcnvlem  38247  psshepw  38399  sprsymrelfo  42072  uspgrsprfo  42081  submgmacs  42129  setrec2fun  42764  setrecsres  42773
  Copyright terms: Public domain W3C validator