Theorem velpw 4559

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 4558	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  sspw  4565  pwss  4577  snsspw  4800  pwpr  4857  pwtp  4858  pwv  4860  pwuni  4901  sspwuni  5055  iinpw  5061  iunpwss  5062  ssextss  5401  pwin  5515  dffr6  5580  sorpsscmpl  7679  iunpw  7716  ordpwsuc  7757  fabexd  7879  fabexgOLD  7881  abexssex  7914  qsss  8713  fsetsspwxp  8790  mapval2  8810  pmsspw  8815  uniixp  8859  fineqvlem  9166  fival  9315  hartogslem1  9447  tskwe  9862  cfval2  10170  cflim3  10172  cflim2  10173  cfslb  10176  compsscnvlem  10280  fin1a2lem13  10322  axdc3lem  10360  fpwwe2lem1  10542  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe  10557  canthwe  10562  axgroth5  10735  axgroth6  10739  wuncn  11081  ishashinf  14386  vdwmc  16906  ramub2  16942  ram0  16950  restsspw  17351  ismred  17521  mremre  17523  acsfn  17582  submgmacs  18642  submacs  18752  subgacs  19090  nsgacs  19091  sylow2alem2  19547  sylow2a  19548  dprdres  19959  subgdmdprd  19965  pgpfac1lem5  20010  subrngmre  20495  subsubrng2  20497  subrgmre  20530  subsubrg2  20532  sdrgacs  20734  lssintcl  20915  lssmre  20917  lssacs  20918  cssmre  21648  istopon  22856  isbasis2g  22892  tgval2  22900  unitg  22911  distop  22939  cldss2  22974  ntreq0  23021  discld  23033  neisspw  23051  restdis  23122  cnntr  23219  isnrm2  23302  cmpcovf  23335  fincmp  23337  cmpsublem  23343  cmpsub  23344  cmpcld  23346  cmpfi  23352  is1stc2  23386  2ndcdisj  23400  llyi  23418  nllyi  23419  nlly2i  23420  llynlly  23421  subislly  23425  restnlly  23426  llyrest  23429  llyidm  23432  nllyidm  23433  islocfin  23461  ptuni2  23520  prdstopn  23572  qtoptop2  23643  qtopuni  23646  tgqtop  23656  isfbas2  23779  isfild  23802  elfg  23815  cfinfil  23837  csdfil  23838  supfil  23839  isufil2  23852  filssufilg  23855  uffix  23865  ufildr  23875  fin1aufil  23876  alexsubb  23990  alexsubALTlem1  23991  alexsubALTlem2  23992  alexsubALT  23995  ptcmplem5  24000  cldsubg  24055  ustfn  24146  ustfilxp  24157  ustn0  24165  dscopn  24517  voliunlem2  25508  vitali  25570  dmcuts  27787  madef  27832  nbuhgr  29416  nbuhgr2vtx1edgblem  29424  shex  31287  dfch2  31482  fpwrelmap  32812  xrsclat  33093  cmpcref  34007  sigaex  34267  sigaval  34268  insiga  34294  sigapisys  34312  sigaldsys  34316  measdivcst  34381  ballotlem2  34646  erdszelem7  35391  erdsze2lem2  35398  rellysconn  35445  dffr5  35948  neibastop2lem  36554  neibastop3  36556  topmeet  36558  topjoin  36559  neifg  36565  bj-snglss  37171  bj-pw0ALT  37250  bj-restpw  37297  bj-imdirval2lem  37387  bj-imdiridlem  37390  dissneqlem  37545  topdifinfeq  37555  pibt2  37622  heibor1lem  38010  psubspset  40004  psubclsetN  40196  lcdlss  41879  ismrcd1  42940  pw2f1ocnv  43279  filnm  43332  hbtlem6  43371  dfno2  43669  elmapintrab  43817  clcnvlem  43864  psshepw  44029  ssclaxsep  45223  pwclaxpow  45225  sprsymrelfo  47743  uspgrsprfo  48394  setrec2fun  49937  setrecsres  49947