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

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  sspw  4553  pwss  4565  snsspw  4788  pwpr  4845  pwtp  4846  pwv  4848  pwuni  4889  sspwuni  5043  iinpw  5049  iunpwss  5050  ssextss  5400  pwin  5515  dffr6  5580  sorpsscmpl  7681  iunpw  7718  ordpwsuc  7759  fabexd  7881  fabexgOLD  7883  abexssex  7916  qsss  8715  fsetsspwxp  8793  mapval2  8813  pmsspw  8818  uniixp  8862  fineqvlem  9169  fival  9318  hartogslem1  9450  tskwe  9865  cfval2  10173  cflim3  10175  cflim2  10176  cfslb  10179  compsscnvlem  10283  fin1a2lem13  10325  axdc3lem  10363  fpwwe2lem1  10545  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe  10560  canthwe  10565  axgroth5  10738  axgroth6  10742  wuncn  11084  ishashinf  14416  vdwmc  16940  ramub2  16976  ram0  16984  restsspw  17385  ismred  17555  mremre  17557  acsfn  17616  submgmacs  18676  submacs  18786  subgacs  19127  nsgacs  19128  sylow2alem2  19584  sylow2a  19585  dprdres  19996  subgdmdprd  20002  pgpfac1lem5  20047  subrngmre  20530  subsubrng2  20532  subrgmre  20565  subsubrg2  20567  sdrgacs  20769  lssintcl  20950  lssmre  20952  lssacs  20953  cssmre  21683  istopon  22887  isbasis2g  22923  tgval2  22931  unitg  22942  distop  22970  cldss2  23005  ntreq0  23052  discld  23064  neisspw  23082  restdis  23153  cnntr  23250  isnrm2  23333  cmpcovf  23366  fincmp  23368  cmpsublem  23374  cmpsub  23375  cmpcld  23377  cmpfi  23383  is1stc2  23417  2ndcdisj  23431  llyi  23449  nllyi  23450  nlly2i  23451  llynlly  23452  subislly  23456  restnlly  23457  llyrest  23460  llyidm  23463  nllyidm  23464  islocfin  23492  ptuni2  23551  prdstopn  23603  qtoptop2  23674  qtopuni  23677  tgqtop  23687  isfbas2  23810  isfild  23833  elfg  23846  cfinfil  23868  csdfil  23869  supfil  23870  isufil2  23883  filssufilg  23886  uffix  23896  ufildr  23906  fin1aufil  23907  alexsubb  24021  alexsubALTlem1  24022  alexsubALTlem2  24023  alexsubALT  24026  ptcmplem5  24031  cldsubg  24086  ustfn  24177  ustfilxp  24188  ustn0  24196  dscopn  24548  voliunlem2  25528  vitali  25590  dmcuts  27797  madef  27842  nbuhgr  29426  nbuhgr2vtx1edgblem  29434  shex  31298  dfch2  31493  fpwrelmap  32821  xrsclat  33086  cmpcref  34010  sigaex  34270  sigaval  34271  insiga  34297  sigapisys  34315  sigaldsys  34319  measdivcst  34384  ballotlem2  34649  erdszelem7  35395  erdsze2lem2  35402  rellysconn  35449  dffr5  35952  neibastop2lem  36558  neibastop3  36560  topmeet  36562  topjoin  36563  neifg  36569  mh-infprim2bi  36745  bj-snglss  37293  bj-pw0ALT  37372  bj-restpw  37420  bj-imdirval2lem  37512  bj-imdiridlem  37515  dissneqlem  37670  topdifinfeq  37680  pibt2  37747  heibor1lem  38144  psubspset  40204  psubclsetN  40396  lcdlss  42079  ismrcd1  43144  pw2f1ocnv  43483  filnm  43536  hbtlem6  43575  dfno2  43873  elmapintrab  44021  clcnvlem  44068  psshepw  44233  ssclaxsep  45427  pwclaxpow  45429  sprsymrelfo  47969  uspgrsprfo  48636  setrec2fun  50179  setrecsres  50189