Theorem velpw 4490

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

Syntax hints:   ↔ wb 209   ∈ wcel 2113   ⊆ wss 3841  𝒫 cpw 4485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-pw 4487

This theorem is referenced by:  elpwgOLD  4492  sspw  4498  pwss  4510  snsspw  4727  pwpr  4787  pwtp  4788  pwv  4790  pwuni  4832  sspwuni  4982  iinpw  4988  iunpwss  4989  ssextss  5309  pwin  5419  pwunssOLD  5420  sorpsscmpl  7472  iunpw  7506  ordpwsuc  7543  fabexg  7658  abexssex  7689  qsss  8382  fsetsspwxp  8456  mapval2  8475  pmsspw  8480  uniixp  8524  fineqvlem  8804  fival  8942  hartogslem1  9072  tskwe  9445  cfval2  9753  cflim3  9755  cflim2  9756  cfslb  9759  compsscnvlem  9863  fin1a2lem13  9905  axdc3lem  9943  fpwwe2lem1  10124  fpwwe2lem10  10133  fpwwe2lem11  10134  fpwwe  10139  canthwe  10144  axgroth5  10317  axgroth6  10321  wuncn  10663  ishashinf  13908  vdwmc  16407  ramub2  16443  ram0  16451  restsspw  16801  ismred  16969  mremre  16971  acsfn  17026  submacs  18100  subgacs  18424  nsgacs  18425  sylow2alem2  18854  sylow2a  18855  dprdres  19262  subgdmdprd  19268  pgpfac1lem5  19313  subrgmre  19671  subsubrg2  19674  sdrgacs  19692  lssintcl  19848  lssmre  19850  lssacs  19851  cssmre  20502  istopon  21656  isbasis2g  21692  tgval2  21700  unitg  21711  distop  21739  cldss2  21774  ntreq0  21821  discld  21833  neisspw  21851  restdis  21922  cnntr  22019  isnrm2  22102  cmpcovf  22135  fincmp  22137  cmpsublem  22143  cmpsub  22144  cmpcld  22146  cmpfi  22152  is1stc2  22186  2ndcdisj  22200  llyi  22218  nllyi  22219  nlly2i  22220  llynlly  22221  subislly  22225  restnlly  22226  llyrest  22229  llyidm  22232  nllyidm  22233  islocfin  22261  ptuni2  22320  prdstopn  22372  qtoptop2  22443  qtopuni  22446  tgqtop  22456  isfbas2  22579  isfild  22602  elfg  22615  cfinfil  22637  csdfil  22638  supfil  22639  isufil2  22652  filssufilg  22655  uffix  22665  ufildr  22675  fin1aufil  22676  alexsubb  22790  alexsubALTlem1  22791  alexsubALTlem2  22792  alexsubALT  22795  ptcmplem5  22800  cldsubg  22855  ustfn  22946  ustfilxp  22957  ustn0  22965  dscopn  23319  voliunlem2  24296  vitali  24358  nbuhgr  27277  nbuhgr2vtx1edgblem  27285  shex  29139  dfch2  29334  fpwrelmap  30635  xrsclat  30858  cmpcref  31364  sigaex  31640  sigaval  31641  insiga  31667  sigapisys  31685  sigaldsys  31689  measdivcst  31754  ballotlem2  32017  erdszelem7  32722  erdsze2lem2  32729  rellysconn  32776  dffr5  33284  dmscut  33638  madef  33673  neibastop2lem  34179  neibastop3  34181  topmeet  34183  topjoin  34184  neifg  34190  bj-snglss  34772  bj-pw0ALT  34834  bj-restpw  34873  bj-imdirval2lem  34963  bj-imdiridlem  34966  dissneqlem  35123  topdifinfeq  35133  pibt2  35200  heibor1lem  35579  psubspset  37370  psubclsetN  37562  lcdlss  39245  ismrcd1  40076  pw2f1ocnv  40415  filnm  40471  hbtlem6  40510  elmapintrab  40713  clcnvlem  40760  psshepw  40926  sprsymrelfo  44467  uspgrsprfo  44828  submgmacs  44876  setrec2fun  45835  setrecsres  45844