Theorem velpw 4571

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  sspw  4577  pwss  4589  snsspw  4811  pwpr  4868  pwtp  4869  pwv  4871  pwuni  4912  sspwuni  5067  iinpw  5073  iunpwss  5074  ssextss  5416  pwin  5532  dffr6  5597  sorpsscmpl  7713  iunpw  7750  ordpwsuc  7793  fabexd  7916  fabexgOLD  7918  abexssex  7952  qsss  8752  fsetsspwxp  8829  mapval2  8848  pmsspw  8853  uniixp  8897  fineqvlem  9216  fival  9370  hartogslem1  9502  tskwe  9910  cfval2  10220  cflim3  10222  cflim2  10223  cfslb  10226  compsscnvlem  10330  fin1a2lem13  10372  axdc3lem  10410  fpwwe2lem1  10591  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe  10606  canthwe  10611  axgroth5  10784  axgroth6  10788  wuncn  11130  ishashinf  14435  vdwmc  16956  ramub2  16992  ram0  17000  restsspw  17401  ismred  17570  mremre  17572  acsfn  17627  submgmacs  18651  submacs  18761  subgacs  19100  nsgacs  19101  sylow2alem2  19555  sylow2a  19556  dprdres  19967  subgdmdprd  19973  pgpfac1lem5  20018  subrngmre  20478  subsubrng2  20480  subrgmre  20513  subsubrg2  20515  sdrgacs  20717  lssintcl  20877  lssmre  20879  lssacs  20880  cssmre  21609  istopon  22806  isbasis2g  22842  tgval2  22850  unitg  22861  distop  22889  cldss2  22924  ntreq0  22971  discld  22983  neisspw  23001  restdis  23072  cnntr  23169  isnrm2  23252  cmpcovf  23285  fincmp  23287  cmpsublem  23293  cmpsub  23294  cmpcld  23296  cmpfi  23302  is1stc2  23336  2ndcdisj  23350  llyi  23368  nllyi  23369  nlly2i  23370  llynlly  23371  subislly  23375  restnlly  23376  llyrest  23379  llyidm  23382  nllyidm  23383  islocfin  23411  ptuni2  23470  prdstopn  23522  qtoptop2  23593  qtopuni  23596  tgqtop  23606  isfbas2  23729  isfild  23752  elfg  23765  cfinfil  23787  csdfil  23788  supfil  23789  isufil2  23802  filssufilg  23805  uffix  23815  ufildr  23825  fin1aufil  23826  alexsubb  23940  alexsubALTlem1  23941  alexsubALTlem2  23942  alexsubALT  23945  ptcmplem5  23950  cldsubg  24005  ustfn  24096  ustfilxp  24107  ustn0  24115  dscopn  24468  voliunlem2  25459  vitali  25521  dmscut  27730  madef  27771  nbuhgr  29277  nbuhgr2vtx1edgblem  29285  shex  31148  dfch2  31343  fpwrelmap  32663  xrsclat  32956  cmpcref  33847  sigaex  34107  sigaval  34108  insiga  34134  sigapisys  34152  sigaldsys  34156  measdivcst  34221  ballotlem2  34487  erdszelem7  35191  erdsze2lem2  35198  rellysconn  35245  dffr5  35748  neibastop2lem  36355  neibastop3  36357  topmeet  36359  topjoin  36360  neifg  36366  bj-snglss  36965  bj-pw0ALT  37044  bj-restpw  37087  bj-imdirval2lem  37177  bj-imdiridlem  37180  dissneqlem  37335  topdifinfeq  37345  pibt2  37412  heibor1lem  37810  psubspset  39745  psubclsetN  39937  lcdlss  41620  ismrcd1  42693  pw2f1ocnv  43033  filnm  43086  hbtlem6  43125  dfno2  43424  elmapintrab  43572  clcnvlem  43619  psshepw  43784  ssclaxsep  44979  pwclaxpow  44981  sprsymrelfo  47502  uspgrsprfo  48140  setrec2fun  49685  setrecsres  49695