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

Theorem velpw 4547
Description: Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
velpw (𝑥 ∈ 𝒫 𝐴𝑥𝐴)

Proof of Theorem velpw
StepHypRef Expression
1 vex 3498 . 2 𝑥 ∈ V
21elpw 4546 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wcel 2110  wss 3936  𝒫 cpw 4539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3943  df-ss 3952  df-pw 4541
This theorem is referenced by:  elpwgOLD  4549  pwss  4559  snsspw  4769  pwpr  4826  pwtp  4827  pwv  4829  pwuni  4868  sspwuni  5015  iinpw  5021  iunpwss  5022  ssextss  5339  pwin  5447  pwunssOLD  5449  sorpsscmpl  7454  iunpw  7487  ordpwsuc  7524  fabexg  7633  abexssex  7665  qsss  8352  mapval2  8430  pmsspw  8435  uniixp  8479  fineqvlem  8726  fival  8870  hartogslem1  9000  tskwe  9373  cfval2  9676  cflim3  9678  cflim2  9679  cfslb  9682  compsscnvlem  9786  fin1a2lem13  9828  axdc3lem  9866  fpwwe2lem1  10047  fpwwe2lem11  10056  fpwwe2lem12  10057  fpwwe  10062  canthwe  10067  axgroth5  10240  axgroth6  10244  wuncn  10586  ishashinf  13815  vdwmc  16308  ramub2  16344  ram0  16352  restsspw  16699  ismred  16867  mremre  16869  acsfn  16924  submacs  17985  subgacs  18307  nsgacs  18308  sylow2alem2  18737  sylow2a  18738  dprdres  19144  subgdmdprd  19150  pgpfac1lem5  19195  subrgmre  19553  subsubrg2  19556  sdrgacs  19574  lssintcl  19730  lssmre  19732  lssacs  19733  cssmre  20831  istopon  21514  isbasis2g  21550  tgval2  21558  unitg  21569  distop  21597  cldss2  21632  ntreq0  21679  discld  21691  neisspw  21709  restdis  21780  cnntr  21877  isnrm2  21960  cmpcovf  21993  fincmp  21995  cmpsublem  22001  cmpsub  22002  cmpcld  22004  cmpfi  22010  is1stc2  22044  2ndcdisj  22058  llyi  22076  nllyi  22077  nlly2i  22078  llynlly  22079  subislly  22083  restnlly  22084  llyrest  22087  llyidm  22090  nllyidm  22091  islocfin  22119  ptuni2  22178  prdstopn  22230  qtoptop2  22301  qtopuni  22304  tgqtop  22314  isfbas2  22437  isfild  22460  elfg  22473  cfinfil  22495  csdfil  22496  supfil  22497  isufil2  22510  filssufilg  22513  uffix  22523  ufildr  22533  fin1aufil  22534  alexsubb  22648  alexsubALTlem1  22649  alexsubALTlem2  22650  alexsubALT  22653  ptcmplem5  22658  cldsubg  22713  ustfn  22804  ustfilxp  22815  ustn0  22823  dscopn  23177  voliunlem2  24146  vitali  24208  nbuhgr  27119  nbuhgr2vtx1edgblem  27127  shex  28983  dfch2  29178  fpwrelmap  30463  xrsclat  30662  cmpcref  31109  sigaex  31364  sigaval  31365  insiga  31391  sigapisys  31409  sigaldsys  31413  measdivcst  31478  ballotlem2  31741  erdszelem7  32439  erdsze2lem2  32446  rellysconn  32493  dffr5  32984  dmscut  33267  neibastop2lem  33703  neibastop3  33705  topmeet  33707  topjoin  33708  neifg  33714  bj-snglss  34277  bj-restpw  34377  bj-imdirval2  34467  bj-imdirid  34469  dissneqlem  34615  topdifinfeq  34625  pibt2  34692  heibor1lem  35081  psubspset  36874  psubclsetN  37066  lcdlss  38749  ismrcd1  39288  pw2f1ocnv  39627  filnm  39683  hbtlem6  39722  elmapintrab  39929  clcnvlem  39976  psshepw  40127  sprsymrelfo  43652  uspgrsprfo  44016  submgmacs  44064  setrec2fun  44788  setrecsres  44797
  Copyright terms: Public domain W3C validator