Theorem velpw 4609

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 3481	. 2 ⊢ 𝑥 ∈ V
2	1	elpw 4608	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2105   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-pw 4606

This theorem is referenced by:  sspw  4615  pwss  4627  snsspw  4848  pwpr  4905  pwtp  4906  pwv  4908  pwuni  4949  sspwuni  5104  iinpw  5110  iunpwss  5111  ssextss  5463  pwin  5578  dffr6  5643  sorpsscmpl  7752  iunpw  7789  ordpwsuc  7834  fabexd  7957  fabexgOLD  7959  abexssex  7993  qsss  8816  fsetsspwxp  8891  mapval2  8910  pmsspw  8915  uniixp  8959  fineqvlem  9295  fival  9449  hartogslem1  9579  tskwe  9987  cfval2  10297  cflim3  10299  cflim2  10300  cfslb  10303  compsscnvlem  10407  fin1a2lem13  10449  axdc3lem  10487  fpwwe2lem1  10668  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe  10683  canthwe  10688  axgroth5  10861  axgroth6  10865  wuncn  11207  ishashinf  14498  vdwmc  17011  ramub2  17047  ram0  17055  restsspw  17477  ismred  17646  mremre  17648  acsfn  17703  submgmacs  18742  submacs  18852  subgacs  19191  nsgacs  19192  sylow2alem2  19650  sylow2a  19651  dprdres  20062  subgdmdprd  20068  pgpfac1lem5  20113  subrngmre  20578  subsubrng2  20580  subrgmre  20613  subsubrg2  20615  sdrgacs  20818  lssintcl  20979  lssmre  20981  lssacs  20982  cssmre  21728  istopon  22933  isbasis2g  22970  tgval2  22978  unitg  22989  distop  23017  cldss2  23053  ntreq0  23100  discld  23112  neisspw  23130  restdis  23201  cnntr  23298  isnrm2  23381  cmpcovf  23414  fincmp  23416  cmpsublem  23422  cmpsub  23423  cmpcld  23425  cmpfi  23431  is1stc2  23465  2ndcdisj  23479  llyi  23497  nllyi  23498  nlly2i  23499  llynlly  23500  subislly  23504  restnlly  23505  llyrest  23508  llyidm  23511  nllyidm  23512  islocfin  23540  ptuni2  23599  prdstopn  23651  qtoptop2  23722  qtopuni  23725  tgqtop  23735  isfbas2  23858  isfild  23881  elfg  23894  cfinfil  23916  csdfil  23917  supfil  23918  isufil2  23931  filssufilg  23934  uffix  23944  ufildr  23954  fin1aufil  23955  alexsubb  24069  alexsubALTlem1  24070  alexsubALTlem2  24071  alexsubALT  24074  ptcmplem5  24079  cldsubg  24134  ustfn  24225  ustfilxp  24236  ustn0  24244  dscopn  24601  voliunlem2  25599  vitali  25661  dmscut  27870  madef  27909  nbuhgr  29374  nbuhgr2vtx1edgblem  29382  shex  31240  dfch2  31435  fpwrelmap  32750  xrsclat  32995  cmpcref  33810  sigaex  34090  sigaval  34091  insiga  34117  sigapisys  34135  sigaldsys  34139  measdivcst  34204  ballotlem2  34469  erdszelem7  35181  erdsze2lem2  35188  rellysconn  35235  dffr5  35733  neibastop2lem  36342  neibastop3  36344  topmeet  36346  topjoin  36347  neifg  36353  bj-snglss  36952  bj-pw0ALT  37031  bj-restpw  37074  bj-imdirval2lem  37164  bj-imdiridlem  37167  dissneqlem  37322  topdifinfeq  37332  pibt2  37399  heibor1lem  37795  psubspset  39726  psubclsetN  39918  lcdlss  41601  ismrcd1  42685  pw2f1ocnv  43025  filnm  43078  hbtlem6  43117  dfno2  43417  elmapintrab  43565  clcnvlem  43612  psshepw  43777  ssclaxsep  44946  sprsymrelfo  47421  uspgrsprfo  47991  setrec2fun  48922  setrecsres  48932