Theorem velpw 4502

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

Syntax hints:   ↔ wb 209   ∈ wcel 2111   ⊆ wss 3881  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  elpwgOLD  4504  sspw  4510  pwss  4522  snsspw  4735  pwpr  4794  pwtp  4795  pwv  4797  pwuni  4837  sspwuni  4985  iinpw  4991  iunpwss  4992  ssextss  5311  pwin  5419  pwunssOLD  5420  sorpsscmpl  7440  iunpw  7473  ordpwsuc  7510  fabexg  7621  abexssex  7653  qsss  8341  mapval2  8419  pmsspw  8424  uniixp  8468  fineqvlem  8716  fival  8860  hartogslem1  8990  tskwe  9363  cfval2  9671  cflim3  9673  cflim2  9674  cfslb  9677  compsscnvlem  9781  fin1a2lem13  9823  axdc3lem  9861  fpwwe2lem1  10042  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe  10057  canthwe  10062  axgroth5  10235  axgroth6  10239  wuncn  10581  ishashinf  13817  vdwmc  16304  ramub2  16340  ram0  16348  restsspw  16697  ismred  16865  mremre  16867  acsfn  16922  submacs  17983  subgacs  18305  nsgacs  18306  sylow2alem2  18735  sylow2a  18736  dprdres  19143  subgdmdprd  19149  pgpfac1lem5  19194  subrgmre  19552  subsubrg2  19555  sdrgacs  19573  lssintcl  19729  lssmre  19731  lssacs  19732  cssmre  20382  istopon  21517  isbasis2g  21553  tgval2  21561  unitg  21572  distop  21600  cldss2  21635  ntreq0  21682  discld  21694  neisspw  21712  restdis  21783  cnntr  21880  isnrm2  21963  cmpcovf  21996  fincmp  21998  cmpsublem  22004  cmpsub  22005  cmpcld  22007  cmpfi  22013  is1stc2  22047  2ndcdisj  22061  llyi  22079  nllyi  22080  nlly2i  22081  llynlly  22082  subislly  22086  restnlly  22087  llyrest  22090  llyidm  22093  nllyidm  22094  islocfin  22122  ptuni2  22181  prdstopn  22233  qtoptop2  22304  qtopuni  22307  tgqtop  22317  isfbas2  22440  isfild  22463  elfg  22476  cfinfil  22498  csdfil  22499  supfil  22500  isufil2  22513  filssufilg  22516  uffix  22526  ufildr  22536  fin1aufil  22537  alexsubb  22651  alexsubALTlem1  22652  alexsubALTlem2  22653  alexsubALT  22656  ptcmplem5  22661  cldsubg  22716  ustfn  22807  ustfilxp  22818  ustn0  22826  dscopn  23180  voliunlem2  24155  vitali  24217  nbuhgr  27133  nbuhgr2vtx1edgblem  27141  shex  28995  dfch2  29190  fpwrelmap  30495  xrsclat  30714  cmpcref  31203  sigaex  31479  sigaval  31480  insiga  31506  sigapisys  31524  sigaldsys  31528  measdivcst  31593  ballotlem2  31856  erdszelem7  32557  erdsze2lem2  32564  rellysconn  32611  dffr5  33102  dmscut  33385  neibastop2lem  33821  neibastop3  33823  topmeet  33825  topjoin  33826  neifg  33832  bj-snglss  34406  bj-pw0ALT  34466  bj-restpw  34507  bj-imdirval2lem  34597  bj-imdiridlem  34600  dissneqlem  34757  topdifinfeq  34767  pibt2  34834  heibor1lem  35247  psubspset  37040  psubclsetN  37232  lcdlss  38915  ismrcd1  39639  pw2f1ocnv  39978  filnm  40034  hbtlem6  40073  elmapintrab  40276  clcnvlem  40323  psshepw  40489  sprsymrelfo  44014  uspgrsprfo  44376  submgmacs  44424  setrec2fun  45222  setrecsres  45231