Theorem velpw 4570

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106   ⊆ wss 3913  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  sspw  4576  pwss  4588  snsspw  4807  pwpr  4864  pwtp  4865  pwv  4867  pwuni  4911  sspwuni  5065  iinpw  5071  iunpwss  5072  ssextss  5415  pwin  5532  dffr6  5596  sorpsscmpl  7676  iunpw  7710  ordpwsuc  7755  fabexg  7876  abexssex  7908  qsss  8724  fsetsspwxp  8798  mapval2  8817  pmsspw  8822  uniixp  8866  fineqvlem  9213  fival  9357  hartogslem1  9487  tskwe  9895  cfval2  10205  cflim3  10207  cflim2  10208  cfslb  10211  compsscnvlem  10315  fin1a2lem13  10357  axdc3lem  10395  fpwwe2lem1  10576  fpwwe2lem10  10585  fpwwe2lem11  10586  fpwwe  10591  canthwe  10596  axgroth5  10769  axgroth6  10773  wuncn  11115  ishashinf  14374  vdwmc  16861  ramub2  16897  ram0  16905  restsspw  17327  ismred  17496  mremre  17498  acsfn  17553  submacs  18651  subgacs  18977  nsgacs  18978  sylow2alem2  19414  sylow2a  19415  dprdres  19821  subgdmdprd  19827  pgpfac1lem5  19872  subrgmre  20295  subsubrg2  20298  sdrgacs  20324  lssintcl  20482  lssmre  20484  lssacs  20485  cssmre  21134  istopon  22298  isbasis2g  22335  tgval2  22343  unitg  22354  distop  22382  cldss2  22418  ntreq0  22465  discld  22477  neisspw  22495  restdis  22566  cnntr  22663  isnrm2  22746  cmpcovf  22779  fincmp  22781  cmpsublem  22787  cmpsub  22788  cmpcld  22790  cmpfi  22796  is1stc2  22830  2ndcdisj  22844  llyi  22862  nllyi  22863  nlly2i  22864  llynlly  22865  subislly  22869  restnlly  22870  llyrest  22873  llyidm  22876  nllyidm  22877  islocfin  22905  ptuni2  22964  prdstopn  23016  qtoptop2  23087  qtopuni  23090  tgqtop  23100  isfbas2  23223  isfild  23246  elfg  23259  cfinfil  23281  csdfil  23282  supfil  23283  isufil2  23296  filssufilg  23299  uffix  23309  ufildr  23319  fin1aufil  23320  alexsubb  23434  alexsubALTlem1  23435  alexsubALTlem2  23436  alexsubALT  23439  ptcmplem5  23444  cldsubg  23499  ustfn  23590  ustfilxp  23601  ustn0  23609  dscopn  23966  voliunlem2  24952  vitali  25014  dmscut  27193  madef  27229  nbuhgr  28354  nbuhgr2vtx1edgblem  28362  shex  30217  dfch2  30412  fpwrelmap  31718  xrsclat  31941  cmpcref  32520  sigaex  32798  sigaval  32799  insiga  32825  sigapisys  32843  sigaldsys  32847  measdivcst  32912  ballotlem2  33177  erdszelem7  33878  erdsze2lem2  33885  rellysconn  33932  dffr5  34413  neibastop2lem  34908  neibastop3  34910  topmeet  34912  topjoin  34913  neifg  34919  bj-snglss  35514  bj-pw0ALT  35593  bj-restpw  35636  bj-imdirval2lem  35726  bj-imdiridlem  35729  dissneqlem  35884  topdifinfeq  35894  pibt2  35961  heibor1lem  36341  psubspset  38280  psubclsetN  38472  lcdlss  40155  ismrcd1  41079  pw2f1ocnv  41419  filnm  41475  hbtlem6  41514  dfno2  41822  elmapintrab  41970  clcnvlem  42017  psshepw  42182  sprsymrelfo  45809  uspgrsprfo  46170  submgmacs  46218  setrec2fun  47257  setrecsres  47267