Theorem velpw 4565

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  sspw  4571  pwv  4578  pwss  4585  snsspw  4804  pwpr  4833  pwtp  4834  pwuni  4911  sspwuni  5065  iinpw  5071  iunpwss  5072  ssextss  5428  pwin  5549  dffr6  5614  sorpsscmpl  7782  iunpw  7817  ordpwsuc  7860  fabexd  7983  abexssex  8016  qsss  8834  fsetsspwxp  8913  mapval2  8938  pmsspw  8943  uniixp  8987  fineqvlem  9295  fival  9441  hartogslem1  9573  setrec2fun  10010  tskwe  10068  cfval2  10377  cflim3  10379  cflim2  10380  cfslb  10383  compsscnvlem  10487  fin1a2lem13  10529  axdc3lem  10567  fpwwe2lem1  10755  fpwwe2lem10  10764  fpwwe2lem11  10765  fpwwe  10770  canthwe  10775  axgroth5  10948  axgroth6  10952  wuncn  11294  ishashinf  14649  vdwmc  17200  ramub2  17236  ram0  17244  restsspw  17652  ismred  17822  mremre  17824  acsfn  17883  submgmacs  18956  submacs  19073  subgacs  19421  nsgacs  19422  sylow2alem2  19883  sylow2a  19884  dprdres  20295  subgdmdprd  20301  pgpfac1lem5  20346  subrngmre  20865  subsubrng2  20867  subrgmre  20900  subsubrg2  20902  sdrgacs  21109  lssintcl  21290  lssmre  21292  lssacs  21293  cssmre  22054  istopon  23285  isbasis2g  23321  tgval2  23329  unitg  23340  distop  23368  cldss2  23403  ntreq0  23450  discld  23462  neisspw  23480  restdis  23551  cnntr  23648  isnrm2  23731  cmpcovf  23764  fincmp  23766  cmpsublem  23772  cmpsub  23773  cmpcld  23775  cmpfi  23781  is1stc2  23815  2ndcdisj  23830  llyi  23848  nllyi  23849  nlly2i  23850  llynlly  23851  subislly  23855  restnlly  23856  llyrest  23859  llyidm  23862  nllyidm  23863  islocfin  23891  ptuni2  23950  prdstopn  24002  qtoptop2  24073  qtopuni  24076  tgqtop  24086  isfbas2  24209  isfild  24232  elfg  24245  cfinfil  24267  csdfil  24268  supfil  24269  isufil2  24282  filssufilg  24285  uffix  24295  ufildr  24305  fin1aufil  24306  alexsubb  24420  alexsubALTlem1  24421  alexsubALTlem2  24422  alexsubALT  24425  ptcmplem5  24430  cldsubg  24485  ustfn  24576  ustfilxp  24587  ustn0  24595  dscopn  24947  voliunlem2  25927  vitali  25989  dmcuts  28234  madef  28279  nbuhgr  29981  nbuhgr2vtx1edgblem  29989  shex  31871  dfch2  32066  fpwrelmap  33421  xrsclat  33671  cmpcref  34593  sigaex  34853  sigaval  34854  insiga  34881  sigapisys  34899  sigaldsys  34903  measdivcst  34968  ballotlem2  35232  abweex  35842  erdszelem7  36170  erdsze2lem2  36177  rellysconn  36224  neibastop2lem  37363  neibastop3  37365  topmeet  37367  topjoin  37368  neifg  37374  mh-infprim2bi  37550  bj-snglss  38098  bj-pw0ALT  38234  bj-restpw  38283  bj-imdirval2lem  38371  bj-imdiridlem  38374  dissneqlem  38531  topdifinfeq  38541  pibt2  38608  heibor1lem  39009  psubspset  41067  psubclsetN  41259  lcdlss  42942  ismrcd1  43975  pw2f1ocnv  44310  filnm  44358  hbtlem6  44396  dfno2  44690  elmapintrab  44838  clcnvlem  44884  psshepw  45049  ssclaxsep  46236  pwclaxpow  46238  sprsymrelfo  48852  uspgrsprfo  49519  setrecsres  51201