Theorem velpw 4555

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111   ⊆ wss 3902  𝒫 cpw 4550

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-pw 4552

This theorem is referenced by:  sspw  4561  pwss  4573  snsspw  4796  pwpr  4853  pwtp  4854  pwv  4856  pwuni  4896  sspwuni  5048  iinpw  5054  iunpwss  5055  ssextss  5394  pwin  5507  dffr6  5572  sorpsscmpl  7667  iunpw  7704  ordpwsuc  7745  fabexd  7867  fabexgOLD  7869  abexssex  7902  qsss  8700  fsetsspwxp  8777  mapval2  8796  pmsspw  8801  uniixp  8845  fineqvlem  9150  fival  9296  hartogslem1  9428  tskwe  9843  cfval2  10151  cflim3  10153  cflim2  10154  cfslb  10157  compsscnvlem  10261  fin1a2lem13  10303  axdc3lem  10341  fpwwe2lem1  10522  fpwwe2lem10  10531  fpwwe2lem11  10532  fpwwe  10537  canthwe  10542  axgroth5  10715  axgroth6  10719  wuncn  11061  ishashinf  14370  vdwmc  16890  ramub2  16926  ram0  16934  restsspw  17335  ismred  17504  mremre  17506  acsfn  17565  submgmacs  18625  submacs  18735  subgacs  19074  nsgacs  19075  sylow2alem2  19531  sylow2a  19532  dprdres  19943  subgdmdprd  19949  pgpfac1lem5  19994  subrngmre  20478  subsubrng2  20480  subrgmre  20513  subsubrg2  20515  sdrgacs  20717  lssintcl  20898  lssmre  20900  lssacs  20901  cssmre  21631  istopon  22828  isbasis2g  22864  tgval2  22872  unitg  22883  distop  22911  cldss2  22946  ntreq0  22993  discld  23005  neisspw  23023  restdis  23094  cnntr  23191  isnrm2  23274  cmpcovf  23307  fincmp  23309  cmpsublem  23315  cmpsub  23316  cmpcld  23318  cmpfi  23324  is1stc2  23358  2ndcdisj  23372  llyi  23390  nllyi  23391  nlly2i  23392  llynlly  23393  subislly  23397  restnlly  23398  llyrest  23401  llyidm  23404  nllyidm  23405  islocfin  23433  ptuni2  23492  prdstopn  23544  qtoptop2  23615  qtopuni  23618  tgqtop  23628  isfbas2  23751  isfild  23774  elfg  23787  cfinfil  23809  csdfil  23810  supfil  23811  isufil2  23824  filssufilg  23827  uffix  23837  ufildr  23847  fin1aufil  23848  alexsubb  23962  alexsubALTlem1  23963  alexsubALTlem2  23964  alexsubALT  23967  ptcmplem5  23972  cldsubg  24027  ustfn  24118  ustfilxp  24129  ustn0  24137  dscopn  24489  voliunlem2  25480  vitali  25542  dmscut  27753  madef  27798  nbuhgr  29322  nbuhgr2vtx1edgblem  29330  shex  31190  dfch2  31385  fpwrelmap  32714  xrsclat  32990  cmpcref  33861  sigaex  34121  sigaval  34122  insiga  34148  sigapisys  34166  sigaldsys  34170  measdivcst  34235  ballotlem2  34500  erdszelem7  35239  erdsze2lem2  35246  rellysconn  35293  dffr5  35796  neibastop2lem  36400  neibastop3  36402  topmeet  36404  topjoin  36405  neifg  36411  bj-snglss  37010  bj-pw0ALT  37089  bj-restpw  37132  bj-imdirval2lem  37222  bj-imdiridlem  37225  dissneqlem  37380  topdifinfeq  37390  pibt2  37457  heibor1lem  37855  psubspset  39789  psubclsetN  39981  lcdlss  41664  ismrcd1  42737  pw2f1ocnv  43076  filnm  43129  hbtlem6  43168  dfno2  43467  elmapintrab  43615  clcnvlem  43662  psshepw  43827  ssclaxsep  45021  pwclaxpow  45023  sprsymrelfo  47534  uspgrsprfo  48185  setrec2fun  49730  setrecsres  49740