Theorem velpw 4557

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141   ⊆ wss 3902  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-pw 4554

This theorem is referenced by:  sspw  4563  pwss  4576  snsspw  4799  pwpr  4856  pwtp  4857  pwv  4859  pwuni  4901  sspwuni  5054  iinpw  5060  iunpwss  5061  ssextss  5417  pwin  5534  dffr6  5599  sorpsscmpl  7711  iunpw  7748  ordpwsuc  7789  fabexd  7912  abexssex  7945  qsss  8750  fsetsspwxp  8827  mapval2  8847  pmsspw  8852  uniixp  8896  fineqvlem  9203  fival  9351  hartogslem1  9483  tskwe  9901  cfval2  10210  cflim3  10212  cflim2  10213  cfslb  10216  compsscnvlem  10320  fin1a2lem13  10362  axdc3lem  10400  fpwwe2lem1  10582  fpwwe2lem10  10591  fpwwe2lem11  10592  fpwwe  10597  canthwe  10602  axgroth5  10775  axgroth6  10779  wuncn  11121  ishashinf  14469  vdwmc  17004  ramub2  17040  ram0  17048  restsspw  17450  ismred  17620  mremre  17622  acsfn  17681  submgmacs  18741  submacs  18851  subgacs  19192  nsgacs  19193  sylow2alem2  19648  sylow2a  19649  dprdres  20060  subgdmdprd  20066  pgpfac1lem5  20111  subrngmre  20598  subsubrng2  20600  subrgmre  20633  subsubrg2  20635  sdrgacs  20837  lssintcl  21018  lssmre  21020  lssacs  21021  cssmre  21732  istopon  22959  isbasis2g  22995  tgval2  23003  unitg  23014  distop  23042  cldss2  23077  ntreq0  23124  discld  23136  neisspw  23154  restdis  23225  cnntr  23322  isnrm2  23405  cmpcovf  23438  fincmp  23440  cmpsublem  23446  cmpsub  23447  cmpcld  23449  cmpfi  23455  is1stc2  23489  2ndcdisj  23503  llyi  23521  nllyi  23522  nlly2i  23523  llynlly  23524  subislly  23528  restnlly  23529  llyrest  23532  llyidm  23535  nllyidm  23536  islocfin  23564  ptuni2  23623  prdstopn  23675  qtoptop2  23746  qtopuni  23749  tgqtop  23759  isfbas2  23882  isfild  23905  elfg  23918  cfinfil  23940  csdfil  23941  supfil  23942  isufil2  23955  filssufilg  23958  uffix  23968  ufildr  23978  fin1aufil  23979  alexsubb  24093  alexsubALTlem1  24094  alexsubALTlem2  24095  alexsubALT  24098  ptcmplem5  24103  cldsubg  24158  ustfn  24249  ustfilxp  24260  ustn0  24268  dscopn  24620  voliunlem2  25600  vitali  25662  dmcuts  27871  madef  27916  nbuhgr  29500  nbuhgr2vtx1edgblem  29508  shex  31371  dfch2  31566  fpwrelmap  32895  xrsclat  33149  cmpcref  34107  sigaex  34367  sigaval  34368  insiga  34394  sigapisys  34412  sigaldsys  34416  measdivcst  34481  ballotlem2  34746  erdszelem7  35507  erdsze2lem2  35514  rellysconn  35561  dffr5  36064  neibastop2lem  36680  neibastop3  36682  topmeet  36684  topjoin  36685  neifg  36691  mh-infprim2bi  36867  bj-snglss  37415  bj-pw0ALT  37494  bj-restpw  37542  bj-imdirval2lem  37634  bj-imdiridlem  37637  dissneqlem  37794  topdifinfeq  37804  pibt2  37871  heibor1lem  38268  psubspset  40328  psubclsetN  40520  lcdlss  42203  ismrcd1  43239  pw2f1ocnv  43574  filnm  43627  hbtlem6  43666  dfno2  43964  elmapintrab  44112  clcnvlem  44159  psshepw  44324  ssclaxsep  45518  pwclaxpow  45520  sprsymrelfo  48063  uspgrsprfo  48730  setrec2fun  50273  setrecsres  50283