Theorem velpw 4541

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-pw 4538

This theorem is referenced by:  sspw  4547  pwss  4559  snsspw  4782  pwpr  4839  pwtp  4840  pwv  4842  pwuni  4883  sspwuni  5036  iinpw  5042  iunpwss  5043  ssextss  5399  pwin  5516  dffr6  5581  sorpsscmpl  7684  iunpw  7721  ordpwsuc  7762  fabexd  7884  fabexgOLD  7886  abexssex  7919  qsss  8719  fsetsspwxp  8797  mapval2  8817  pmsspw  8822  uniixp  8866  fineqvlem  9173  fival  9322  hartogslem1  9454  tskwe  9872  cfval2  10180  cflim3  10182  cflim2  10183  cfslb  10186  compsscnvlem  10290  fin1a2lem13  10332  axdc3lem  10370  fpwwe2lem1  10552  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe  10567  canthwe  10572  axgroth5  10745  axgroth6  10749  wuncn  11091  ishashinf  14423  vdwmc  16947  ramub2  16983  ram0  16991  restsspw  17392  ismred  17562  mremre  17564  acsfn  17623  submgmacs  18683  submacs  18793  subgacs  19134  nsgacs  19135  sylow2alem2  19591  sylow2a  19592  dprdres  20003  subgdmdprd  20009  pgpfac1lem5  20054  subrngmre  20541  subsubrng2  20543  subrgmre  20576  subsubrg2  20578  sdrgacs  20780  lssintcl  20961  lssmre  20963  lssacs  20964  cssmre  21675  istopon  22902  isbasis2g  22938  tgval2  22946  unitg  22957  distop  22985  cldss2  23020  ntreq0  23067  discld  23079  neisspw  23097  restdis  23168  cnntr  23265  isnrm2  23348  cmpcovf  23381  fincmp  23383  cmpsublem  23389  cmpsub  23390  cmpcld  23392  cmpfi  23398  is1stc2  23432  2ndcdisj  23446  llyi  23464  nllyi  23465  nlly2i  23466  llynlly  23467  subislly  23471  restnlly  23472  llyrest  23475  llyidm  23478  nllyidm  23479  islocfin  23507  ptuni2  23566  prdstopn  23618  qtoptop2  23689  qtopuni  23692  tgqtop  23702  isfbas2  23825  isfild  23848  elfg  23861  cfinfil  23883  csdfil  23884  supfil  23885  isufil2  23898  filssufilg  23901  uffix  23911  ufildr  23921  fin1aufil  23922  alexsubb  24036  alexsubALTlem1  24037  alexsubALTlem2  24038  alexsubALT  24041  ptcmplem5  24046  cldsubg  24101  ustfn  24192  ustfilxp  24203  ustn0  24211  dscopn  24563  voliunlem2  25543  vitali  25605  dmcuts  27808  madef  27853  nbuhgr  29437  nbuhgr2vtx1edgblem  29445  shex  31308  dfch2  31503  fpwrelmap  32832  xrsclat  33097  cmpcref  34041  sigaex  34301  sigaval  34302  insiga  34328  sigapisys  34346  sigaldsys  34350  measdivcst  34415  ballotlem2  34680  erdszelem7  35432  erdsze2lem2  35439  rellysconn  35486  dffr5  35989  neibastop2lem  36595  neibastop3  36597  topmeet  36599  topjoin  36600  neifg  36606  mh-infprim2bi  36782  bj-snglss  37330  bj-pw0ALT  37409  bj-restpw  37457  bj-imdirval2lem  37549  bj-imdiridlem  37552  dissneqlem  37709  topdifinfeq  37719  pibt2  37786  heibor1lem  38183  psubspset  40243  psubclsetN  40435  lcdlss  42118  ismrcd1  43154  pw2f1ocnv  43489  filnm  43542  hbtlem6  43581  dfno2  43879  elmapintrab  44027  clcnvlem  44074  psshepw  44239  ssclaxsep  45433  pwclaxpow  45435  sprsymrelfo  47979  uspgrsprfo  48646  setrec2fun  50189  setrecsres  50199