Theorem velpw 4607

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

Syntax hints:   ↔ wb 205   ∈ wcel 2105   ⊆ wss 3948  𝒫 cpw 4602

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  sspw  4613  pwss  4625  snsspw  4845  pwpr  4902  pwtp  4903  pwv  4905  pwuni  4949  sspwuni  5103  iinpw  5109  iunpwss  5110  ssextss  5453  pwin  5570  dffr6  5634  sorpsscmpl  7728  iunpw  7762  ordpwsuc  7807  fabexg  7929  abexssex  7961  qsss  8778  fsetsspwxp  8853  mapval2  8872  pmsspw  8877  uniixp  8921  fineqvlem  9268  fival  9413  hartogslem1  9543  tskwe  9951  cfval2  10261  cflim3  10263  cflim2  10264  cfslb  10267  compsscnvlem  10371  fin1a2lem13  10413  axdc3lem  10451  fpwwe2lem1  10632  fpwwe2lem10  10641  fpwwe2lem11  10642  fpwwe  10647  canthwe  10652  axgroth5  10825  axgroth6  10829  wuncn  11171  ishashinf  14431  vdwmc  16918  ramub2  16954  ram0  16962  restsspw  17384  ismred  17553  mremre  17555  acsfn  17610  submgmacs  18648  submacs  18750  subgacs  19084  nsgacs  19085  sylow2alem2  19534  sylow2a  19535  dprdres  19946  subgdmdprd  19952  pgpfac1lem5  19997  subrngmre  20458  subsubrng2  20460  subrgmre  20495  subsubrg2  20497  sdrgacs  20648  lssintcl  20807  lssmre  20809  lssacs  20810  cssmre  21556  istopon  22734  isbasis2g  22771  tgval2  22779  unitg  22790  distop  22818  cldss2  22854  ntreq0  22901  discld  22913  neisspw  22931  restdis  23002  cnntr  23099  isnrm2  23182  cmpcovf  23215  fincmp  23217  cmpsublem  23223  cmpsub  23224  cmpcld  23226  cmpfi  23232  is1stc2  23266  2ndcdisj  23280  llyi  23298  nllyi  23299  nlly2i  23300  llynlly  23301  subislly  23305  restnlly  23306  llyrest  23309  llyidm  23312  nllyidm  23313  islocfin  23341  ptuni2  23400  prdstopn  23452  qtoptop2  23523  qtopuni  23526  tgqtop  23536  isfbas2  23659  isfild  23682  elfg  23695  cfinfil  23717  csdfil  23718  supfil  23719  isufil2  23732  filssufilg  23735  uffix  23745  ufildr  23755  fin1aufil  23756  alexsubb  23870  alexsubALTlem1  23871  alexsubALTlem2  23872  alexsubALT  23875  ptcmplem5  23880  cldsubg  23935  ustfn  24026  ustfilxp  24037  ustn0  24045  dscopn  24402  voliunlem2  25400  vitali  25462  dmscut  27657  madef  27696  nbuhgr  29033  nbuhgr2vtx1edgblem  29041  shex  30898  dfch2  31093  fpwrelmap  32391  xrsclat  32614  cmpcref  33294  sigaex  33572  sigaval  33573  insiga  33599  sigapisys  33617  sigaldsys  33621  measdivcst  33686  ballotlem2  33951  erdszelem7  34652  erdsze2lem2  34659  rellysconn  34706  dffr5  35194  neibastop2lem  35709  neibastop3  35711  topmeet  35713  topjoin  35714  neifg  35720  bj-snglss  36315  bj-pw0ALT  36394  bj-restpw  36437  bj-imdirval2lem  36527  bj-imdiridlem  36530  dissneqlem  36685  topdifinfeq  36695  pibt2  36762  heibor1lem  37141  psubspset  39079  psubclsetN  39271  lcdlss  40954  ismrcd1  41899  pw2f1ocnv  42239  filnm  42295  hbtlem6  42334  dfno2  42642  elmapintrab  42790  clcnvlem  42837  psshepw  43002  sprsymrelfo  46624  uspgrsprfo  46985  setrec2fun  47899  setrecsres  47909