Theorem velpw 4535

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  elpwgOLD  4537  sspw  4543  pwss  4555  snsspw  4772  pwpr  4830  pwtp  4831  pwv  4833  pwuni  4875  sspwuni  5025  iinpw  5031  iunpwss  5032  ssextss  5363  pwin  5474  pwunssOLD  5475  dffr6  5538  sorpsscmpl  7565  iunpw  7599  ordpwsuc  7637  fabexg  7755  abexssex  7786  qsss  8525  fsetsspwxp  8599  mapval2  8618  pmsspw  8623  uniixp  8667  fineqvlem  8966  fival  9101  hartogslem1  9231  tskwe  9639  cfval2  9947  cflim3  9949  cflim2  9950  cfslb  9953  compsscnvlem  10057  fin1a2lem13  10099  axdc3lem  10137  fpwwe2lem1  10318  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe  10333  canthwe  10338  axgroth5  10511  axgroth6  10515  wuncn  10857  ishashinf  14105  vdwmc  16607  ramub2  16643  ram0  16651  restsspw  17059  ismred  17228  mremre  17230  acsfn  17285  submacs  18380  subgacs  18704  nsgacs  18705  sylow2alem2  19138  sylow2a  19139  dprdres  19546  subgdmdprd  19552  pgpfac1lem5  19597  subrgmre  19963  subsubrg2  19966  sdrgacs  19984  lssintcl  20141  lssmre  20143  lssacs  20144  cssmre  20810  istopon  21969  isbasis2g  22006  tgval2  22014  unitg  22025  distop  22053  cldss2  22089  ntreq0  22136  discld  22148  neisspw  22166  restdis  22237  cnntr  22334  isnrm2  22417  cmpcovf  22450  fincmp  22452  cmpsublem  22458  cmpsub  22459  cmpcld  22461  cmpfi  22467  is1stc2  22501  2ndcdisj  22515  llyi  22533  nllyi  22534  nlly2i  22535  llynlly  22536  subislly  22540  restnlly  22541  llyrest  22544  llyidm  22547  nllyidm  22548  islocfin  22576  ptuni2  22635  prdstopn  22687  qtoptop2  22758  qtopuni  22761  tgqtop  22771  isfbas2  22894  isfild  22917  elfg  22930  cfinfil  22952  csdfil  22953  supfil  22954  isufil2  22967  filssufilg  22970  uffix  22980  ufildr  22990  fin1aufil  22991  alexsubb  23105  alexsubALTlem1  23106  alexsubALTlem2  23107  alexsubALT  23110  ptcmplem5  23115  cldsubg  23170  ustfn  23261  ustfilxp  23272  ustn0  23280  dscopn  23635  voliunlem2  24620  vitali  24682  nbuhgr  27613  nbuhgr2vtx1edgblem  27621  shex  29475  dfch2  29670  fpwrelmap  30970  xrsclat  31191  cmpcref  31702  sigaex  31978  sigaval  31979  insiga  32005  sigapisys  32023  sigaldsys  32027  measdivcst  32092  ballotlem2  32355  erdszelem7  33059  erdsze2lem2  33066  rellysconn  33113  dffr5  33627  dmscut  33932  madef  33967  neibastop2lem  34476  neibastop3  34478  topmeet  34480  topjoin  34481  neifg  34487  bj-snglss  35087  bj-pw0ALT  35149  bj-restpw  35190  bj-imdirval2lem  35280  bj-imdiridlem  35283  dissneqlem  35438  topdifinfeq  35448  pibt2  35515  heibor1lem  35894  psubspset  37685  psubclsetN  37877  lcdlss  39560  ismrcd1  40436  pw2f1ocnv  40775  filnm  40831  hbtlem6  40870  elmapintrab  41073  clcnvlem  41120  psshepw  41285  sprsymrelfo  44837  uspgrsprfo  45198  submgmacs  45246  setrec2fun  46284  setrecsres  46293