Theorem velpw 4539

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107   ⊆ wss 3888  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  elpwgOLD  4541  sspw  4547  pwss  4559  snsspw  4776  pwpr  4834  pwtp  4835  pwv  4837  pwuni  4879  sspwuni  5030  iinpw  5036  iunpwss  5037  ssextss  5370  pwin  5484  pwunssOLD  5485  dffr6  5548  sorpsscmpl  7596  iunpw  7630  ordpwsuc  7671  fabexg  7790  abexssex  7822  qsss  8576  fsetsspwxp  8650  mapval2  8669  pmsspw  8674  uniixp  8718  fineqvlem  9046  fival  9180  hartogslem1  9310  tskwe  9717  cfval2  10025  cflim3  10027  cflim2  10028  cfslb  10031  compsscnvlem  10135  fin1a2lem13  10177  axdc3lem  10215  fpwwe2lem1  10396  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe  10411  canthwe  10416  axgroth5  10589  axgroth6  10593  wuncn  10935  ishashinf  14186  vdwmc  16688  ramub2  16724  ram0  16732  restsspw  17151  ismred  17320  mremre  17322  acsfn  17377  submacs  18474  subgacs  18798  nsgacs  18799  sylow2alem2  19232  sylow2a  19233  dprdres  19640  subgdmdprd  19646  pgpfac1lem5  19691  subrgmre  20057  subsubrg2  20060  sdrgacs  20078  lssintcl  20235  lssmre  20237  lssacs  20238  cssmre  20907  istopon  22070  isbasis2g  22107  tgval2  22115  unitg  22126  distop  22154  cldss2  22190  ntreq0  22237  discld  22249  neisspw  22267  restdis  22338  cnntr  22435  isnrm2  22518  cmpcovf  22551  fincmp  22553  cmpsublem  22559  cmpsub  22560  cmpcld  22562  cmpfi  22568  is1stc2  22602  2ndcdisj  22616  llyi  22634  nllyi  22635  nlly2i  22636  llynlly  22637  subislly  22641  restnlly  22642  llyrest  22645  llyidm  22648  nllyidm  22649  islocfin  22677  ptuni2  22736  prdstopn  22788  qtoptop2  22859  qtopuni  22862  tgqtop  22872  isfbas2  22995  isfild  23018  elfg  23031  cfinfil  23053  csdfil  23054  supfil  23055  isufil2  23068  filssufilg  23071  uffix  23081  ufildr  23091  fin1aufil  23092  alexsubb  23206  alexsubALTlem1  23207  alexsubALTlem2  23208  alexsubALT  23211  ptcmplem5  23216  cldsubg  23271  ustfn  23362  ustfilxp  23373  ustn0  23381  dscopn  23738  voliunlem2  24724  vitali  24786  nbuhgr  27719  nbuhgr2vtx1edgblem  27727  shex  29583  dfch2  29778  fpwrelmap  31077  xrsclat  31298  cmpcref  31809  sigaex  32087  sigaval  32088  insiga  32114  sigapisys  32132  sigaldsys  32136  measdivcst  32201  ballotlem2  32464  erdszelem7  33168  erdsze2lem2  33175  rellysconn  33222  dffr5  33730  dmscut  34014  madef  34049  neibastop2lem  34558  neibastop3  34560  topmeet  34562  topjoin  34563  neifg  34569  bj-snglss  35169  bj-pw0ALT  35231  bj-restpw  35272  bj-imdirval2lem  35362  bj-imdiridlem  35365  dissneqlem  35520  topdifinfeq  35530  pibt2  35597  heibor1lem  35976  psubspset  37765  psubclsetN  37957  lcdlss  39640  ismrcd1  40527  pw2f1ocnv  40866  filnm  40922  hbtlem6  40961  elmapintrab  41191  clcnvlem  41238  psshepw  41403  sprsymrelfo  44960  uspgrsprfo  45321  submgmacs  45369  setrec2fun  46409  setrecsres  46418