Theorem velpw 4569

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4566

This theorem is referenced by:  sspw  4575  pwss  4588  snsspw  4810  pwpr  4867  pwtp  4868  pwv  4870  pwuni  4912  sspwuni  5067  iinpw  5073  iunpwss  5074  ssextss  5432  pwin  5550  dffr6  5615  sorpsscmpl  7729  iunpw  7766  ordpwsuc  7807  fabexd  7930  abexssex  7963  qsss  8769  fsetsspwxp  8846  mapval2  8866  pmsspw  8871  uniixp  8915  fineqvlem  9222  fival  9368  hartogslem1  9500  tskwe  9932  cfval2  10240  cflim3  10242  cflim2  10243  cfslb  10246  compsscnvlem  10350  fin1a2lem13  10392  axdc3lem  10430  fpwwe2lem1  10612  fpwwe2lem10  10621  fpwwe2lem11  10622  fpwwe  10627  canthwe  10632  axgroth5  10805  axgroth6  10809  wuncn  11151  ishashinf  14496  vdwmc  17034  ramub2  17070  ram0  17078  restsspw  17480  ismred  17650  mremre  17652  acsfn  17711  submgmacs  18771  submacs  18882  subgacs  19223  nsgacs  19224  sylow2alem2  19684  sylow2a  19685  dprdres  20096  subgdmdprd  20102  pgpfac1lem5  20147  subrngmre  20643  subsubrng2  20645  subrgmre  20678  subsubrg2  20680  sdrgacs  20878  lssintcl  21059  lssmre  21061  lssacs  21062  cssmre  21808  istopon  23034  isbasis2g  23070  tgval2  23078  unitg  23089  distop  23117  cldss2  23152  ntreq0  23199  discld  23211  neisspw  23229  restdis  23300  cnntr  23397  isnrm2  23480  cmpcovf  23513  fincmp  23515  cmpsublem  23521  cmpsub  23522  cmpcld  23524  cmpfi  23530  is1stc2  23564  2ndcdisj  23578  llyi  23596  nllyi  23597  nlly2i  23598  llynlly  23599  subislly  23603  restnlly  23604  llyrest  23607  llyidm  23610  nllyidm  23611  islocfin  23639  ptuni2  23698  prdstopn  23750  qtoptop2  23821  qtopuni  23824  tgqtop  23834  isfbas2  23957  isfild  23980  elfg  23993  cfinfil  24015  csdfil  24016  supfil  24017  isufil2  24030  filssufilg  24033  uffix  24043  ufildr  24053  fin1aufil  24054  alexsubb  24168  alexsubALTlem1  24169  alexsubALTlem2  24170  alexsubALT  24173  ptcmplem5  24178  cldsubg  24233  ustfn  24324  ustfilxp  24335  ustn0  24343  dscopn  24695  voliunlem2  25675  vitali  25737  dmcuts  27946  madef  27991  nbuhgr  29630  nbuhgr2vtx1edgblem  29638  shex  31501  dfch2  31696  fpwrelmap  33015  xrsclat  33268  cmpcref  34181  sigaex  34441  sigaval  34442  insiga  34468  sigapisys  34486  sigaldsys  34490  measdivcst  34555  ballotlem2  34820  erdszelem7  35584  erdsze2lem2  35591  rellysconn  35638  dffr5  36141  neibastop2lem  36756  neibastop3  36758  topmeet  36760  topjoin  36761  neifg  36767  mh-infprim2bi  36943  bj-snglss  37490  bj-pw0ALT  37569  bj-restpw  37617  bj-imdirval2lem  37709  bj-imdiridlem  37712  dissneqlem  37869  topdifinfeq  37879  pibt2  37946  heibor1lem  38343  psubspset  40403  psubclsetN  40595  lcdlss  42278  ismrcd1  43314  pw2f1ocnv  43649  filnm  43702  hbtlem6  43741  dfno2  44039  elmapintrab  44187  clcnvlem  44234  psshepw  44399  ssclaxsep  45576  pwclaxpow  45578  sprsymrelfo  48128  uspgrsprfo  48795  setrec2fun  50348  setrecsres  50358