Theorem velpw 4557

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141   ⊆ wss 3902  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-pw 4554

This theorem is referenced by:  sspw  4563  pwss  4576  snsspw  4799  pwpr  4856  pwtp  4857  pwv  4859  pwuni  4901  sspwuni  5054  iinpw  5060  iunpwss  5061  ssextss  5417  pwin  5534  dffr6  5599  sorpsscmpl  7712  iunpw  7749  ordpwsuc  7790  fabexd  7913  abexssex  7946  qsss  8751  fsetsspwxp  8828  mapval2  8848  pmsspw  8853  uniixp  8897  fineqvlem  9204  fival  9352  hartogslem1  9484  tskwe  9902  cfval2  10211  cflim3  10213  cflim2  10214  cfslb  10217  compsscnvlem  10321  fin1a2lem13  10363  axdc3lem  10401  fpwwe2lem1  10583  fpwwe2lem10  10592  fpwwe2lem11  10593  fpwwe  10598  canthwe  10603  axgroth5  10776  axgroth6  10780  wuncn  11122  ishashinf  14470  vdwmc  17005  ramub2  17041  ram0  17049  restsspw  17451  ismred  17621  mremre  17623  acsfn  17682  submgmacs  18742  submacs  18852  subgacs  19193  nsgacs  19194  sylow2alem2  19649  sylow2a  19650  dprdres  20061  subgdmdprd  20067  pgpfac1lem5  20112  subrngmre  20599  subsubrng2  20601  subrgmre  20634  subsubrg2  20636  sdrgacs  20838  lssintcl  21019  lssmre  21021  lssacs  21022  cssmre  21733  istopon  22960  isbasis2g  22996  tgval2  23004  unitg  23015  distop  23043  cldss2  23078  ntreq0  23125  discld  23137  neisspw  23155  restdis  23226  cnntr  23323  isnrm2  23406  cmpcovf  23439  fincmp  23441  cmpsublem  23447  cmpsub  23448  cmpcld  23450  cmpfi  23456  is1stc2  23490  2ndcdisj  23504  llyi  23522  nllyi  23523  nlly2i  23524  llynlly  23525  subislly  23529  restnlly  23530  llyrest  23533  llyidm  23536  nllyidm  23537  islocfin  23565  ptuni2  23624  prdstopn  23676  qtoptop2  23747  qtopuni  23750  tgqtop  23760  isfbas2  23883  isfild  23906  elfg  23919  cfinfil  23941  csdfil  23942  supfil  23943  isufil2  23956  filssufilg  23959  uffix  23969  ufildr  23979  fin1aufil  23980  alexsubb  24094  alexsubALTlem1  24095  alexsubALTlem2  24096  alexsubALT  24099  ptcmplem5  24104  cldsubg  24159  ustfn  24250  ustfilxp  24261  ustn0  24269  dscopn  24621  voliunlem2  25601  vitali  25663  dmcuts  27872  madef  27917  nbuhgr  29501  nbuhgr2vtx1edgblem  29509  shex  31372  dfch2  31567  fpwrelmap  32896  xrsclat  33150  cmpcref  34108  sigaex  34368  sigaval  34369  insiga  34395  sigapisys  34413  sigaldsys  34417  measdivcst  34482  ballotlem2  34747  erdszelem7  35508  erdsze2lem2  35515  rellysconn  35562  dffr5  36065  neibastop2lem  36681  neibastop3  36683  topmeet  36685  topjoin  36686  neifg  36692  mh-infprim2bi  36868  bj-snglss  37416  bj-pw0ALT  37495  bj-restpw  37543  bj-imdirval2lem  37635  bj-imdiridlem  37638  dissneqlem  37795  topdifinfeq  37805  pibt2  37872  heibor1lem  38269  psubspset  40329  psubclsetN  40521  lcdlss  42204  ismrcd1  43240  pw2f1ocnv  43575  filnm  43628  hbtlem6  43667  dfno2  43965  elmapintrab  44113  clcnvlem  44160  psshepw  44325  ssclaxsep  45519  pwclaxpow  45521  sprsymrelfo  48064  uspgrsprfo  48731  setrec2fun  50274  setrecsres  50284