Theorem velpw 4564

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3911  𝒫 cpw 4559

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  sspw  4570  pwss  4582  snsspw  4804  pwpr  4861  pwtp  4862  pwv  4864  pwuni  4905  sspwuni  5059  iinpw  5065  iunpwss  5066  ssextss  5408  pwin  5522  dffr6  5587  sorpsscmpl  7690  iunpw  7727  ordpwsuc  7770  fabexd  7893  fabexgOLD  7895  abexssex  7928  qsss  8726  fsetsspwxp  8803  mapval2  8822  pmsspw  8827  uniixp  8871  fineqvlem  9185  fival  9339  hartogslem1  9471  tskwe  9879  cfval2  10189  cflim3  10191  cflim2  10192  cfslb  10195  compsscnvlem  10299  fin1a2lem13  10341  axdc3lem  10379  fpwwe2lem1  10560  fpwwe2lem10  10569  fpwwe2lem11  10570  fpwwe  10575  canthwe  10580  axgroth5  10753  axgroth6  10757  wuncn  11099  ishashinf  14404  vdwmc  16925  ramub2  16961  ram0  16969  restsspw  17370  ismred  17539  mremre  17541  acsfn  17596  submgmacs  18620  submacs  18730  subgacs  19069  nsgacs  19070  sylow2alem2  19524  sylow2a  19525  dprdres  19936  subgdmdprd  19942  pgpfac1lem5  19987  subrngmre  20447  subsubrng2  20449  subrgmre  20482  subsubrg2  20484  sdrgacs  20686  lssintcl  20846  lssmre  20848  lssacs  20849  cssmre  21578  istopon  22775  isbasis2g  22811  tgval2  22819  unitg  22830  distop  22858  cldss2  22893  ntreq0  22940  discld  22952  neisspw  22970  restdis  23041  cnntr  23138  isnrm2  23221  cmpcovf  23254  fincmp  23256  cmpsublem  23262  cmpsub  23263  cmpcld  23265  cmpfi  23271  is1stc2  23305  2ndcdisj  23319  llyi  23337  nllyi  23338  nlly2i  23339  llynlly  23340  subislly  23344  restnlly  23345  llyrest  23348  llyidm  23351  nllyidm  23352  islocfin  23380  ptuni2  23439  prdstopn  23491  qtoptop2  23562  qtopuni  23565  tgqtop  23575  isfbas2  23698  isfild  23721  elfg  23734  cfinfil  23756  csdfil  23757  supfil  23758  isufil2  23771  filssufilg  23774  uffix  23784  ufildr  23794  fin1aufil  23795  alexsubb  23909  alexsubALTlem1  23910  alexsubALTlem2  23911  alexsubALT  23914  ptcmplem5  23919  cldsubg  23974  ustfn  24065  ustfilxp  24076  ustn0  24084  dscopn  24437  voliunlem2  25428  vitali  25490  dmscut  27699  madef  27740  nbuhgr  29246  nbuhgr2vtx1edgblem  29254  shex  31114  dfch2  31309  fpwrelmap  32629  xrsclat  32922  cmpcref  33813  sigaex  34073  sigaval  34074  insiga  34100  sigapisys  34118  sigaldsys  34122  measdivcst  34187  ballotlem2  34453  erdszelem7  35157  erdsze2lem2  35164  rellysconn  35211  dffr5  35714  neibastop2lem  36321  neibastop3  36323  topmeet  36325  topjoin  36326  neifg  36332  bj-snglss  36931  bj-pw0ALT  37010  bj-restpw  37053  bj-imdirval2lem  37143  bj-imdiridlem  37146  dissneqlem  37301  topdifinfeq  37311  pibt2  37378  heibor1lem  37776  psubspset  39711  psubclsetN  39903  lcdlss  41586  ismrcd1  42659  pw2f1ocnv  42999  filnm  43052  hbtlem6  43091  dfno2  43390  elmapintrab  43538  clcnvlem  43585  psshepw  43750  ssclaxsep  44945  pwclaxpow  44947  sprsymrelfo  47471  uspgrsprfo  48109  setrec2fun  49654  setrecsres  49664