Theorem velpw 4605

Description: Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
velpw	⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Proof of Theorem velpw

Step	Hyp	Ref	Expression
1		vex 3484	. 2 ⊢ 𝑥 ∈ V
2	1	elpw 4604	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3951  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602

This theorem is referenced by:  sspw  4611  pwss  4623  snsspw  4844  pwpr  4901  pwtp  4902  pwv  4904  pwuni  4945  sspwuni  5100  iinpw  5106  iunpwss  5107  ssextss  5458  pwin  5574  dffr6  5640  sorpsscmpl  7754  iunpw  7791  ordpwsuc  7835  fabexd  7959  fabexgOLD  7961  abexssex  7995  qsss  8818  fsetsspwxp  8893  mapval2  8912  pmsspw  8917  uniixp  8961  fineqvlem  9298  fival  9452  hartogslem1  9582  tskwe  9990  cfval2  10300  cflim3  10302  cflim2  10303  cfslb  10306  compsscnvlem  10410  fin1a2lem13  10452  axdc3lem  10490  fpwwe2lem1  10671  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe  10686  canthwe  10691  axgroth5  10864  axgroth6  10868  wuncn  11210  ishashinf  14502  vdwmc  17016  ramub2  17052  ram0  17060  restsspw  17476  ismred  17645  mremre  17647  acsfn  17702  submgmacs  18730  submacs  18840  subgacs  19179  nsgacs  19180  sylow2alem2  19636  sylow2a  19637  dprdres  20048  subgdmdprd  20054  pgpfac1lem5  20099  subrngmre  20562  subsubrng2  20564  subrgmre  20597  subsubrg2  20599  sdrgacs  20802  lssintcl  20962  lssmre  20964  lssacs  20965  cssmre  21711  istopon  22918  isbasis2g  22955  tgval2  22963  unitg  22974  distop  23002  cldss2  23038  ntreq0  23085  discld  23097  neisspw  23115  restdis  23186  cnntr  23283  isnrm2  23366  cmpcovf  23399  fincmp  23401  cmpsublem  23407  cmpsub  23408  cmpcld  23410  cmpfi  23416  is1stc2  23450  2ndcdisj  23464  llyi  23482  nllyi  23483  nlly2i  23484  llynlly  23485  subislly  23489  restnlly  23490  llyrest  23493  llyidm  23496  nllyidm  23497  islocfin  23525  ptuni2  23584  prdstopn  23636  qtoptop2  23707  qtopuni  23710  tgqtop  23720  isfbas2  23843  isfild  23866  elfg  23879  cfinfil  23901  csdfil  23902  supfil  23903  isufil2  23916  filssufilg  23919  uffix  23929  ufildr  23939  fin1aufil  23940  alexsubb  24054  alexsubALTlem1  24055  alexsubALTlem2  24056  alexsubALT  24059  ptcmplem5  24064  cldsubg  24119  ustfn  24210  ustfilxp  24221  ustn0  24229  dscopn  24586  voliunlem2  25586  vitali  25648  dmscut  27856  madef  27895  nbuhgr  29360  nbuhgr2vtx1edgblem  29368  shex  31231  dfch2  31426  fpwrelmap  32744  xrsclat  33013  cmpcref  33849  sigaex  34111  sigaval  34112  insiga  34138  sigapisys  34156  sigaldsys  34160  measdivcst  34225  ballotlem2  34491  erdszelem7  35202  erdsze2lem2  35209  rellysconn  35256  dffr5  35754  neibastop2lem  36361  neibastop3  36363  topmeet  36365  topjoin  36366  neifg  36372  bj-snglss  36971  bj-pw0ALT  37050  bj-restpw  37093  bj-imdirval2lem  37183  bj-imdiridlem  37186  dissneqlem  37341  topdifinfeq  37351  pibt2  37418  heibor1lem  37816  psubspset  39746  psubclsetN  39938  lcdlss  41621  ismrcd1  42709  pw2f1ocnv  43049  filnm  43102  hbtlem6  43141  dfno2  43441  elmapintrab  43589  clcnvlem  43636  psshepw  43801  ssclaxsep  44999  pwclaxpow  45001  sprsymrelfo  47484  uspgrsprfo  48064  setrec2fun  49211  setrecsres  49221