Theorem velpw 4568

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  sspw  4574  pwss  4586  snsspw  4808  pwpr  4865  pwtp  4866  pwv  4868  pwuni  4909  sspwuni  5064  iinpw  5070  iunpwss  5071  ssextss  5413  pwin  5529  dffr6  5594  sorpsscmpl  7710  iunpw  7747  ordpwsuc  7790  fabexd  7913  fabexgOLD  7915  abexssex  7949  qsss  8749  fsetsspwxp  8826  mapval2  8845  pmsspw  8850  uniixp  8894  fineqvlem  9209  fival  9363  hartogslem1  9495  tskwe  9903  cfval2  10213  cflim3  10215  cflim2  10216  cfslb  10219  compsscnvlem  10323  fin1a2lem13  10365  axdc3lem  10403  fpwwe2lem1  10584  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe  10599  canthwe  10604  axgroth5  10777  axgroth6  10781  wuncn  11123  ishashinf  14428  vdwmc  16949  ramub2  16985  ram0  16993  restsspw  17394  ismred  17563  mremre  17565  acsfn  17620  submgmacs  18644  submacs  18754  subgacs  19093  nsgacs  19094  sylow2alem2  19548  sylow2a  19549  dprdres  19960  subgdmdprd  19966  pgpfac1lem5  20011  subrngmre  20471  subsubrng2  20473  subrgmre  20506  subsubrg2  20508  sdrgacs  20710  lssintcl  20870  lssmre  20872  lssacs  20873  cssmre  21602  istopon  22799  isbasis2g  22835  tgval2  22843  unitg  22854  distop  22882  cldss2  22917  ntreq0  22964  discld  22976  neisspw  22994  restdis  23065  cnntr  23162  isnrm2  23245  cmpcovf  23278  fincmp  23280  cmpsublem  23286  cmpsub  23287  cmpcld  23289  cmpfi  23295  is1stc2  23329  2ndcdisj  23343  llyi  23361  nllyi  23362  nlly2i  23363  llynlly  23364  subislly  23368  restnlly  23369  llyrest  23372  llyidm  23375  nllyidm  23376  islocfin  23404  ptuni2  23463  prdstopn  23515  qtoptop2  23586  qtopuni  23589  tgqtop  23599  isfbas2  23722  isfild  23745  elfg  23758  cfinfil  23780  csdfil  23781  supfil  23782  isufil2  23795  filssufilg  23798  uffix  23808  ufildr  23818  fin1aufil  23819  alexsubb  23933  alexsubALTlem1  23934  alexsubALTlem2  23935  alexsubALT  23938  ptcmplem5  23943  cldsubg  23998  ustfn  24089  ustfilxp  24100  ustn0  24108  dscopn  24461  voliunlem2  25452  vitali  25514  dmscut  27723  madef  27764  nbuhgr  29270  nbuhgr2vtx1edgblem  29278  shex  31141  dfch2  31336  fpwrelmap  32656  xrsclat  32949  cmpcref  33840  sigaex  34100  sigaval  34101  insiga  34127  sigapisys  34145  sigaldsys  34149  measdivcst  34214  ballotlem2  34480  erdszelem7  35184  erdsze2lem2  35191  rellysconn  35238  dffr5  35741  neibastop2lem  36348  neibastop3  36350  topmeet  36352  topjoin  36353  neifg  36359  bj-snglss  36958  bj-pw0ALT  37037  bj-restpw  37080  bj-imdirval2lem  37170  bj-imdiridlem  37173  dissneqlem  37328  topdifinfeq  37338  pibt2  37405  heibor1lem  37803  psubspset  39738  psubclsetN  39930  lcdlss  41613  ismrcd1  42686  pw2f1ocnv  43026  filnm  43079  hbtlem6  43118  dfno2  43417  elmapintrab  43565  clcnvlem  43612  psshepw  43777  ssclaxsep  44972  pwclaxpow  44974  sprsymrelfo  47498  uspgrsprfo  48136  setrec2fun  49681  setrecsres  49691