Theorem velpw 4562

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  sspw  4568  pwss  4581  snsspw  4804  pwpr  4861  pwtp  4862  pwv  4864  pwuni  4906  sspwuni  5060  iinpw  5066  iunpwss  5067  ssextss  5421  pwin  5542  dffr6  5607  sorpsscmpl  7748  iunpw  7783  ordpwsuc  7824  fabexd  7947  abexssex  7980  qsss  8789  fsetsspwxp  8868  mapval2  8893  pmsspw  8898  uniixp  8942  fineqvlem  9250  fival  9397  hartogslem1  9529  setrec2fun  9966  tskwe  10024  cfval2  10331  cflim3  10333  cflim2  10334  cfslb  10337  compsscnvlem  10441  fin1a2lem13  10483  axdc3lem  10521  fpwwe2lem1  10709  fpwwe2lem10  10718  fpwwe2lem11  10719  fpwwe  10724  canthwe  10729  axgroth5  10902  axgroth6  10906  wuncn  11248  ishashinf  14601  vdwmc  17149  ramub2  17185  ram0  17193  restsspw  17595  ismred  17765  mremre  17767  acsfn  17826  submgmacs  18899  submacs  19016  subgacs  19364  nsgacs  19365  sylow2alem2  19825  sylow2a  19826  dprdres  20237  subgdmdprd  20243  pgpfac1lem5  20288  subrngmre  20807  subsubrng2  20809  subrgmre  20842  subsubrg2  20844  sdrgacs  21051  lssintcl  21232  lssmre  21234  lssacs  21235  cssmre  21992  istopon  23223  isbasis2g  23259  tgval2  23267  unitg  23278  distop  23306  cldss2  23341  ntreq0  23388  discld  23400  neisspw  23418  restdis  23489  cnntr  23586  isnrm2  23669  cmpcovf  23702  fincmp  23704  cmpsublem  23710  cmpsub  23711  cmpcld  23713  cmpfi  23719  is1stc2  23753  2ndcdisj  23768  llyi  23786  nllyi  23787  nlly2i  23788  llynlly  23789  subislly  23793  restnlly  23794  llyrest  23797  llyidm  23800  nllyidm  23801  islocfin  23829  ptuni2  23888  prdstopn  23940  qtoptop2  24011  qtopuni  24014  tgqtop  24024  isfbas2  24147  isfild  24170  elfg  24183  cfinfil  24205  csdfil  24206  supfil  24207  isufil2  24220  filssufilg  24223  uffix  24233  ufildr  24243  fin1aufil  24244  alexsubb  24358  alexsubALTlem1  24359  alexsubALTlem2  24360  alexsubALT  24363  ptcmplem5  24368  cldsubg  24423  ustfn  24514  ustfilxp  24525  ustn0  24533  dscopn  24885  voliunlem2  25865  vitali  25927  dmcuts  28170  madef  28215  nbuhgr  29917  nbuhgr2vtx1edgblem  29925  shex  31807  dfch2  32002  fpwrelmap  33318  xrsclat  33565  cmpcref  34475  sigaex  34735  sigaval  34736  insiga  34763  sigapisys  34781  sigaldsys  34785  measdivcst  34850  ballotlem2  35114  erdszelem7  35941  erdsze2lem2  35948  rellysconn  35995  neibastop2lem  37128  neibastop3  37130  topmeet  37132  topjoin  37133  neifg  37139  mh-infprim2bi  37315  bj-snglss  37863  bj-pw0ALT  37944  bj-restpw  37993  bj-imdirval2lem  38083  bj-imdiridlem  38086  dissneqlem  38243  topdifinfeq  38253  pibt2  38320  heibor1lem  38723  psubspset  40781  psubclsetN  40973  lcdlss  42656  ismrcd1  43688  pw2f1ocnv  44023  filnm  44076  hbtlem6  44115  dfno2  44413  elmapintrab  44561  clcnvlem  44608  psshepw  44773  ssclaxsep  45950  pwclaxpow  45952  sprsymrelfo  48548  uspgrsprfo  49215  setrecsres  50764