Theorem velpw 4608

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107   ⊆ wss 3949  𝒫 cpw 4603

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  sspw  4614  pwss  4626  snsspw  4846  pwpr  4903  pwtp  4904  pwv  4906  pwuni  4950  sspwuni  5104  iinpw  5110  iunpwss  5111  ssextss  5454  pwin  5571  dffr6  5635  sorpsscmpl  7724  iunpw  7758  ordpwsuc  7803  fabexg  7925  abexssex  7957  qsss  8772  fsetsspwxp  8847  mapval2  8866  pmsspw  8871  uniixp  8915  fineqvlem  9262  fival  9407  hartogslem1  9537  tskwe  9945  cfval2  10255  cflim3  10257  cflim2  10258  cfslb  10261  compsscnvlem  10365  fin1a2lem13  10407  axdc3lem  10445  fpwwe2lem1  10626  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe  10641  canthwe  10646  axgroth5  10819  axgroth6  10823  wuncn  11165  ishashinf  14424  vdwmc  16911  ramub2  16947  ram0  16955  restsspw  17377  ismred  17546  mremre  17548  acsfn  17603  submacs  18708  subgacs  19041  nsgacs  19042  sylow2alem2  19486  sylow2a  19487  dprdres  19898  subgdmdprd  19904  pgpfac1lem5  19949  subrgmre  20344  subsubrg2  20346  sdrgacs  20417  lssintcl  20575  lssmre  20577  lssacs  20578  cssmre  21246  istopon  22414  isbasis2g  22451  tgval2  22459  unitg  22470  distop  22498  cldss2  22534  ntreq0  22581  discld  22593  neisspw  22611  restdis  22682  cnntr  22779  isnrm2  22862  cmpcovf  22895  fincmp  22897  cmpsublem  22903  cmpsub  22904  cmpcld  22906  cmpfi  22912  is1stc2  22946  2ndcdisj  22960  llyi  22978  nllyi  22979  nlly2i  22980  llynlly  22981  subislly  22985  restnlly  22986  llyrest  22989  llyidm  22992  nllyidm  22993  islocfin  23021  ptuni2  23080  prdstopn  23132  qtoptop2  23203  qtopuni  23206  tgqtop  23216  isfbas2  23339  isfild  23362  elfg  23375  cfinfil  23397  csdfil  23398  supfil  23399  isufil2  23412  filssufilg  23415  uffix  23425  ufildr  23435  fin1aufil  23436  alexsubb  23550  alexsubALTlem1  23551  alexsubALTlem2  23552  alexsubALT  23555  ptcmplem5  23560  cldsubg  23615  ustfn  23706  ustfilxp  23717  ustn0  23725  dscopn  24082  voliunlem2  25068  vitali  25130  dmscut  27312  madef  27351  nbuhgr  28600  nbuhgr2vtx1edgblem  28608  shex  30465  dfch2  30660  fpwrelmap  31958  xrsclat  32181  cmpcref  32830  sigaex  33108  sigaval  33109  insiga  33135  sigapisys  33153  sigaldsys  33157  measdivcst  33222  ballotlem2  33487  erdszelem7  34188  erdsze2lem2  34195  rellysconn  34242  dffr5  34724  neibastop2lem  35245  neibastop3  35247  topmeet  35249  topjoin  35250  neifg  35256  bj-snglss  35851  bj-pw0ALT  35930  bj-restpw  35973  bj-imdirval2lem  36063  bj-imdiridlem  36066  dissneqlem  36221  topdifinfeq  36231  pibt2  36298  heibor1lem  36677  psubspset  38615  psubclsetN  38807  lcdlss  40490  ismrcd1  41436  pw2f1ocnv  41776  filnm  41832  hbtlem6  41871  dfno2  42179  elmapintrab  42327  clcnvlem  42374  psshepw  42539  sprsymrelfo  46165  uspgrsprfo  46526  submgmacs  46574  subrngmre  46741  subsubrng2  46743  setrec2fun  47737  setrecsres  47747