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

Syntax hints:   ↔ wb 209   ∈ wcel 2143   ⊆ wss 3906  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-pw 4565

This theorem is referenced by:  sspw  4574  pwss  4587  snsspw  4810  pwpr  4867  pwtp  4868  pwv  4870  pwuni  4912  sspwuni  5067  iinpw  5073  iunpwss  5074  ssextss  5436  pwin  5554  dffr6  5619  sorpsscmpl  7733  iunpw  7771  ordpwsuc  7812  fabexd  7935  abexssex  7968  qsss  8774  fsetsspwxp  8851  mapval2  8871  pmsspw  8876  uniixp  8920  fineqvlem  9227  fival  9373  hartogslem1  9505  tskwe  9937  cfval2  10245  cflim3  10247  cflim2  10248  cfslb  10251  compsscnvlem  10355  fin1a2lem13  10397  axdc3lem  10435  fpwwe2lem1  10617  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe  10632  canthwe  10637  axgroth5  10810  axgroth6  10814  wuncn  11156  ishashinf  14502  vdwmc  17039  ramub2  17075  ram0  17083  restsspw  17485  ismred  17655  mremre  17657  acsfn  17716  submgmacs  18776  submacs  18887  subgacs  19228  nsgacs  19229  sylow2alem2  19689  sylow2a  19690  dprdres  20101  subgdmdprd  20107  pgpfac1lem5  20152  subrngmre  20648  subsubrng2  20650  subrgmre  20683  subsubrg2  20685  sdrgacs  20885  lssintcl  21066  lssmre  21068  lssacs  21069  cssmre  21824  istopon  23050  isbasis2g  23086  tgval2  23094  unitg  23105  distop  23133  cldss2  23168  ntreq0  23215  discld  23227  neisspw  23245  restdis  23316  cnntr  23413  isnrm2  23496  cmpcovf  23529  fincmp  23531  cmpsublem  23537  cmpsub  23538  cmpcld  23540  cmpfi  23546  is1stc2  23580  2ndcdisj  23594  llyi  23612  nllyi  23613  nlly2i  23614  llynlly  23615  subislly  23619  restnlly  23620  llyrest  23623  llyidm  23626  nllyidm  23627  islocfin  23655  ptuni2  23714  prdstopn  23766  qtoptop2  23837  qtopuni  23840  tgqtop  23850  isfbas2  23973  isfild  23996  elfg  24009  cfinfil  24031  csdfil  24032  supfil  24033  isufil2  24046  filssufilg  24049  uffix  24059  ufildr  24069  fin1aufil  24070  alexsubb  24184  alexsubALTlem1  24185  alexsubALTlem2  24186  alexsubALT  24189  ptcmplem5  24194  cldsubg  24249  ustfn  24340  ustfilxp  24351  ustn0  24359  dscopn  24711  voliunlem2  25691  vitali  25753  dmcuts  27965  madef  28010  nbuhgr  29674  nbuhgr2vtx1edgblem  29682  shex  31545  dfch2  31740  fpwrelmap  33059  xrsclat  33312  cmpcref  34221  sigaex  34481  sigaval  34482  insiga  34508  sigapisys  34526  sigaldsys  34530  measdivcst  34595  ballotlem2  34860  erdszelem7  35670  erdsze2lem2  35677  rellysconn  35724  dffr5  36227  neibastop2lem  36852  neibastop3  36854  topmeet  36856  topjoin  36857  neifg  36863  mh-infprim2bi  37039  bj-snglss  37587  bj-pw0ALT  37666  bj-restpw  37715  bj-imdirval2lem  37807  bj-imdiridlem  37810  dissneqlem  37967  topdifinfeq  37977  pibt2  38044  heibor1lem  38441  psubspset  40499  psubclsetN  40691  lcdlss  42374  ismrcd1  43412  pw2f1ocnv  43747  filnm  43800  hbtlem6  43839  dfno2  44137  elmapintrab  44285  clcnvlem  44332  psshepw  44497  ssclaxsep  45674  pwclaxpow  45676  sprsymrelfo  48229  uspgrsprfo  48896  setrec2fun  50453  setrecsres  50463