Theorem velpw 4561

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  sspw  4567  pwss  4579  snsspw  4802  pwpr  4859  pwtp  4860  pwv  4862  pwuni  4903  sspwuni  5057  iinpw  5063  iunpwss  5064  ssextss  5408  pwin  5523  dffr6  5588  sorpsscmpl  7689  iunpw  7726  ordpwsuc  7767  fabexd  7889  fabexgOLD  7891  abexssex  7924  qsss  8724  fsetsspwxp  8802  mapval2  8822  pmsspw  8827  uniixp  8871  fineqvlem  9178  fival  9327  hartogslem1  9459  tskwe  9874  cfval2  10182  cflim3  10184  cflim2  10185  cfslb  10188  compsscnvlem  10292  fin1a2lem13  10334  axdc3lem  10372  fpwwe2lem1  10554  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe  10569  canthwe  10574  axgroth5  10747  axgroth6  10751  wuncn  11093  ishashinf  14398  vdwmc  16918  ramub2  16954  ram0  16962  restsspw  17363  ismred  17533  mremre  17535  acsfn  17594  submgmacs  18654  submacs  18764  subgacs  19102  nsgacs  19103  sylow2alem2  19559  sylow2a  19560  dprdres  19971  subgdmdprd  19977  pgpfac1lem5  20022  subrngmre  20507  subsubrng2  20509  subrgmre  20542  subsubrg2  20544  sdrgacs  20746  lssintcl  20927  lssmre  20929  lssacs  20930  cssmre  21660  istopon  22868  isbasis2g  22904  tgval2  22912  unitg  22923  distop  22951  cldss2  22986  ntreq0  23033  discld  23045  neisspw  23063  restdis  23134  cnntr  23231  isnrm2  23314  cmpcovf  23347  fincmp  23349  cmpsublem  23355  cmpsub  23356  cmpcld  23358  cmpfi  23364  is1stc2  23398  2ndcdisj  23412  llyi  23430  nllyi  23431  nlly2i  23432  llynlly  23433  subislly  23437  restnlly  23438  llyrest  23441  llyidm  23444  nllyidm  23445  islocfin  23473  ptuni2  23532  prdstopn  23584  qtoptop2  23655  qtopuni  23658  tgqtop  23668  isfbas2  23791  isfild  23814  elfg  23827  cfinfil  23849  csdfil  23850  supfil  23851  isufil2  23864  filssufilg  23867  uffix  23877  ufildr  23887  fin1aufil  23888  alexsubb  24002  alexsubALTlem1  24003  alexsubALTlem2  24004  alexsubALT  24007  ptcmplem5  24012  cldsubg  24067  ustfn  24158  ustfilxp  24169  ustn0  24177  dscopn  24529  voliunlem2  25520  vitali  25582  dmcuts  27799  madef  27844  nbuhgr  29428  nbuhgr2vtx1edgblem  29436  shex  31299  dfch2  31494  fpwrelmap  32822  xrsclat  33103  cmpcref  34027  sigaex  34287  sigaval  34288  insiga  34314  sigapisys  34332  sigaldsys  34336  measdivcst  34401  ballotlem2  34666  erdszelem7  35410  erdsze2lem2  35417  rellysconn  35464  dffr5  35967  neibastop2lem  36573  neibastop3  36575  topmeet  36577  topjoin  36578  neifg  36584  bj-snglss  37215  bj-pw0ALT  37294  bj-restpw  37342  bj-imdirval2lem  37434  bj-imdiridlem  37437  dissneqlem  37592  topdifinfeq  37602  pibt2  37669  heibor1lem  38057  psubspset  40117  psubclsetN  40309  lcdlss  41992  ismrcd1  43052  pw2f1ocnv  43391  filnm  43444  hbtlem6  43483  dfno2  43781  elmapintrab  43929  clcnvlem  43976  psshepw  44141  ssclaxsep  45335  pwclaxpow  45337  sprsymrelfo  47854  uspgrsprfo  48505  setrec2fun  50048  setrecsres  50058