Theorem velpw 4556

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113   ⊆ wss 3898  𝒫 cpw 4551

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-pw 4553

This theorem is referenced by:  sspw  4562  pwss  4574  snsspw  4797  pwpr  4854  pwtp  4855  pwv  4857  pwuni  4898  sspwuni  5052  iinpw  5058  iunpwss  5059  ssextss  5398  pwin  5512  dffr6  5577  sorpsscmpl  7676  iunpw  7713  ordpwsuc  7754  fabexd  7876  fabexgOLD  7878  abexssex  7911  qsss  8709  fsetsspwxp  8786  mapval2  8806  pmsspw  8811  uniixp  8855  fineqvlem  9161  fival  9307  hartogslem1  9439  tskwe  9854  cfval2  10162  cflim3  10164  cflim2  10165  cfslb  10168  compsscnvlem  10272  fin1a2lem13  10314  axdc3lem  10352  fpwwe2lem1  10533  fpwwe2lem10  10542  fpwwe2lem11  10543  fpwwe  10548  canthwe  10553  axgroth5  10726  axgroth6  10730  wuncn  11072  ishashinf  14377  vdwmc  16897  ramub2  16933  ram0  16941  restsspw  17342  ismred  17512  mremre  17514  acsfn  17573  submgmacs  18633  submacs  18743  subgacs  19081  nsgacs  19082  sylow2alem2  19538  sylow2a  19539  dprdres  19950  subgdmdprd  19956  pgpfac1lem5  20001  subrngmre  20486  subsubrng2  20488  subrgmre  20521  subsubrg2  20523  sdrgacs  20725  lssintcl  20906  lssmre  20908  lssacs  20909  cssmre  21639  istopon  22847  isbasis2g  22883  tgval2  22891  unitg  22902  distop  22930  cldss2  22965  ntreq0  23012  discld  23024  neisspw  23042  restdis  23113  cnntr  23210  isnrm2  23293  cmpcovf  23326  fincmp  23328  cmpsublem  23334  cmpsub  23335  cmpcld  23337  cmpfi  23343  is1stc2  23377  2ndcdisj  23391  llyi  23409  nllyi  23410  nlly2i  23411  llynlly  23412  subislly  23416  restnlly  23417  llyrest  23420  llyidm  23423  nllyidm  23424  islocfin  23452  ptuni2  23511  prdstopn  23563  qtoptop2  23634  qtopuni  23637  tgqtop  23647  isfbas2  23770  isfild  23793  elfg  23806  cfinfil  23828  csdfil  23829  supfil  23830  isufil2  23843  filssufilg  23846  uffix  23856  ufildr  23866  fin1aufil  23867  alexsubb  23981  alexsubALTlem1  23982  alexsubALTlem2  23983  alexsubALT  23986  ptcmplem5  23991  cldsubg  24046  ustfn  24137  ustfilxp  24148  ustn0  24156  dscopn  24508  voliunlem2  25499  vitali  25561  dmscut  27772  madef  27817  nbuhgr  29342  nbuhgr2vtx1edgblem  29350  shex  31213  dfch2  31408  fpwrelmap  32740  xrsclat  33021  cmpcref  33935  sigaex  34195  sigaval  34196  insiga  34222  sigapisys  34240  sigaldsys  34244  measdivcst  34309  ballotlem2  34574  erdszelem7  35313  erdsze2lem2  35320  rellysconn  35367  dffr5  35870  neibastop2lem  36476  neibastop3  36478  topmeet  36480  topjoin  36481  neifg  36487  bj-snglss  37087  bj-pw0ALT  37166  bj-restpw  37209  bj-imdirval2lem  37299  bj-imdiridlem  37302  dissneqlem  37457  topdifinfeq  37467  pibt2  37534  heibor1lem  37922  psubspset  39916  psubclsetN  40108  lcdlss  41791  ismrcd1  42855  pw2f1ocnv  43194  filnm  43247  hbtlem6  43286  dfno2  43585  elmapintrab  43733  clcnvlem  43780  psshepw  43945  ssclaxsep  45139  pwclaxpow  45141  sprsymrelfo  47659  uspgrsprfo  48310  setrec2fun  49853  setrecsres  49863