Theorem velpw 4546

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  sspw  4552  pwss  4564  snsspw  4787  pwpr  4844  pwtp  4845  pwv  4847  pwuni  4888  sspwuni  5042  iinpw  5048  iunpwss  5049  ssextss  5405  pwin  5522  dffr6  5587  sorpsscmpl  7688  iunpw  7725  ordpwsuc  7766  fabexd  7888  fabexgOLD  7890  abexssex  7923  qsss  8722  fsetsspwxp  8800  mapval2  8820  pmsspw  8825  uniixp  8869  fineqvlem  9176  fival  9325  hartogslem1  9457  tskwe  9874  cfval2  10182  cflim3  10184  cflim2  10185  cfslb  10188  compsscnvlem  10292  fin1a2lem13  10334  axdc3lem  10372  fpwwe2lem1  10554  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe  10569  canthwe  10574  axgroth5  10747  axgroth6  10751  wuncn  11093  ishashinf  14425  vdwmc  16949  ramub2  16985  ram0  16993  restsspw  17394  ismred  17564  mremre  17566  acsfn  17625  submgmacs  18685  submacs  18795  subgacs  19136  nsgacs  19137  sylow2alem2  19593  sylow2a  19594  dprdres  20005  subgdmdprd  20011  pgpfac1lem5  20056  subrngmre  20539  subsubrng2  20541  subrgmre  20574  subsubrg2  20576  sdrgacs  20778  lssintcl  20959  lssmre  20961  lssacs  20962  cssmre  21673  istopon  22877  isbasis2g  22913  tgval2  22921  unitg  22932  distop  22960  cldss2  22995  ntreq0  23042  discld  23054  neisspw  23072  restdis  23143  cnntr  23240  isnrm2  23323  cmpcovf  23356  fincmp  23358  cmpsublem  23364  cmpsub  23365  cmpcld  23367  cmpfi  23373  is1stc2  23407  2ndcdisj  23421  llyi  23439  nllyi  23440  nlly2i  23441  llynlly  23442  subislly  23446  restnlly  23447  llyrest  23450  llyidm  23453  nllyidm  23454  islocfin  23482  ptuni2  23541  prdstopn  23593  qtoptop2  23664  qtopuni  23667  tgqtop  23677  isfbas2  23800  isfild  23823  elfg  23836  cfinfil  23858  csdfil  23859  supfil  23860  isufil2  23873  filssufilg  23876  uffix  23886  ufildr  23896  fin1aufil  23897  alexsubb  24011  alexsubALTlem1  24012  alexsubALTlem2  24013  alexsubALT  24016  ptcmplem5  24021  cldsubg  24076  ustfn  24167  ustfilxp  24178  ustn0  24186  dscopn  24538  voliunlem2  25518  vitali  25580  dmcuts  27783  madef  27828  nbuhgr  29412  nbuhgr2vtx1edgblem  29420  shex  31283  dfch2  31478  fpwrelmap  32806  xrsclat  33071  cmpcref  33994  sigaex  34254  sigaval  34255  insiga  34281  sigapisys  34299  sigaldsys  34303  measdivcst  34368  ballotlem2  34633  erdszelem7  35379  erdsze2lem2  35386  rellysconn  35433  dffr5  35936  neibastop2lem  36542  neibastop3  36544  topmeet  36546  topjoin  36547  neifg  36553  mh-infprim2bi  36729  bj-snglss  37277  bj-pw0ALT  37356  bj-restpw  37404  bj-imdirval2lem  37496  bj-imdiridlem  37499  dissneqlem  37656  topdifinfeq  37666  pibt2  37733  heibor1lem  38130  psubspset  40190  psubclsetN  40382  lcdlss  42065  ismrcd1  43130  pw2f1ocnv  43465  filnm  43518  hbtlem6  43557  dfno2  43855  elmapintrab  44003  clcnvlem  44050  psshepw  44215  ssclaxsep  45409  pwclaxpow  45411  sprsymrelfo  47957  uspgrsprfo  48624  setrec2fun  50167  setrecsres  50177