Theorem velpw 4627

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  sspw  4633  pwss  4645  snsspw  4869  pwpr  4925  pwtp  4926  pwv  4928  pwuni  4969  sspwuni  5123  iinpw  5129  iunpwss  5130  ssextss  5473  pwin  5589  dffr6  5655  sorpsscmpl  7769  iunpw  7806  ordpwsuc  7851  fabexd  7975  fabexgOLD  7977  abexssex  8011  qsss  8836  fsetsspwxp  8911  mapval2  8930  pmsspw  8935  uniixp  8979  fineqvlem  9325  fival  9481  hartogslem1  9611  tskwe  10019  cfval2  10329  cflim3  10331  cflim2  10332  cfslb  10335  compsscnvlem  10439  fin1a2lem13  10481  axdc3lem  10519  fpwwe2lem1  10700  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe  10715  canthwe  10720  axgroth5  10893  axgroth6  10897  wuncn  11239  ishashinf  14512  vdwmc  17025  ramub2  17061  ram0  17069  restsspw  17491  ismred  17660  mremre  17662  acsfn  17717  submgmacs  18755  submacs  18862  subgacs  19201  nsgacs  19202  sylow2alem2  19660  sylow2a  19661  dprdres  20072  subgdmdprd  20078  pgpfac1lem5  20123  subrngmre  20588  subsubrng2  20590  subrgmre  20625  subsubrg2  20627  sdrgacs  20824  lssintcl  20985  lssmre  20987  lssacs  20988  cssmre  21734  istopon  22939  isbasis2g  22976  tgval2  22984  unitg  22995  distop  23023  cldss2  23059  ntreq0  23106  discld  23118  neisspw  23136  restdis  23207  cnntr  23304  isnrm2  23387  cmpcovf  23420  fincmp  23422  cmpsublem  23428  cmpsub  23429  cmpcld  23431  cmpfi  23437  is1stc2  23471  2ndcdisj  23485  llyi  23503  nllyi  23504  nlly2i  23505  llynlly  23506  subislly  23510  restnlly  23511  llyrest  23514  llyidm  23517  nllyidm  23518  islocfin  23546  ptuni2  23605  prdstopn  23657  qtoptop2  23728  qtopuni  23731  tgqtop  23741  isfbas2  23864  isfild  23887  elfg  23900  cfinfil  23922  csdfil  23923  supfil  23924  isufil2  23937  filssufilg  23940  uffix  23950  ufildr  23960  fin1aufil  23961  alexsubb  24075  alexsubALTlem1  24076  alexsubALTlem2  24077  alexsubALT  24080  ptcmplem5  24085  cldsubg  24140  ustfn  24231  ustfilxp  24242  ustn0  24250  dscopn  24607  voliunlem2  25605  vitali  25667  dmscut  27874  madef  27913  nbuhgr  29378  nbuhgr2vtx1edgblem  29386  shex  31244  dfch2  31439  fpwrelmap  32747  xrsclat  32994  cmpcref  33796  sigaex  34074  sigaval  34075  insiga  34101  sigapisys  34119  sigaldsys  34123  measdivcst  34188  ballotlem2  34453  erdszelem7  35165  erdsze2lem2  35172  rellysconn  35219  dffr5  35716  neibastop2lem  36326  neibastop3  36328  topmeet  36330  topjoin  36331  neifg  36337  bj-snglss  36936  bj-pw0ALT  37015  bj-restpw  37058  bj-imdirval2lem  37148  bj-imdiridlem  37151  dissneqlem  37306  topdifinfeq  37316  pibt2  37383  heibor1lem  37769  psubspset  39701  psubclsetN  39893  lcdlss  41576  ismrcd1  42654  pw2f1ocnv  42994  filnm  43047  hbtlem6  43086  dfno2  43390  elmapintrab  43538  clcnvlem  43585  psshepw  43750  sprsymrelfo  47371  uspgrsprfo  47871  setrec2fun  48784  setrecsres  48794