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 3454	. 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5428  pwin  5546  dffr6  5611  sorpsscmpl  7735  iunpw  7770  ordpwsuc  7811  fabexd  7934  abexssex  7967  qsss  8775  fsetsspwxp  8854  mapval2  8879  pmsspw  8884  uniixp  8928  fineqvlem  9236  fival  9382  hartogslem1  9514  tskwe  9955  cfval2  10262  cflim3  10264  cflim2  10265  cfslb  10268  compsscnvlem  10372  fin1a2lem13  10414  axdc3lem  10452  fpwwe2lem1  10640  fpwwe2lem10  10649  fpwwe2lem11  10650  fpwwe  10655  canthwe  10660  axgroth5  10833  axgroth6  10837  wuncn  11179  ishashinf  14528  vdwmc  17070  ramub2  17106  ram0  17114  restsspw  17516  ismred  17686  mremre  17688  acsfn  17747  submgmacs  18819  submacs  18936  subgacs  19284  nsgacs  19285  sylow2alem2  19745  sylow2a  19746  dprdres  20157  subgdmdprd  20163  pgpfac1lem5  20208  subrngmre  20724  subsubrng2  20726  subrgmre  20759  subsubrg2  20761  sdrgacs  20967  lssintcl  21148  lssmre  21150  lssacs  21151  cssmre  21906  istopon  23137  isbasis2g  23173  tgval2  23181  unitg  23192  distop  23220  cldss2  23255  ntreq0  23302  discld  23314  neisspw  23332  restdis  23403  cnntr  23500  isnrm2  23583  cmpcovf  23616  fincmp  23618  cmpsublem  23624  cmpsub  23625  cmpcld  23627  cmpfi  23633  is1stc2  23667  2ndcdisj  23682  llyi  23700  nllyi  23701  nlly2i  23702  llynlly  23703  subislly  23707  restnlly  23708  llyrest  23711  llyidm  23714  nllyidm  23715  islocfin  23743  ptuni2  23802  prdstopn  23854  qtoptop2  23925  qtopuni  23928  tgqtop  23938  isfbas2  24061  isfild  24084  elfg  24097  cfinfil  24119  csdfil  24120  supfil  24121  isufil2  24134  filssufilg  24137  uffix  24147  ufildr  24157  fin1aufil  24158  alexsubb  24272  alexsubALTlem1  24273  alexsubALTlem2  24274  alexsubALT  24277  ptcmplem5  24282  cldsubg  24337  ustfn  24428  ustfilxp  24439  ustn0  24447  dscopn  24799  voliunlem2  25779  vitali  25841  dmcuts  28056  madef  28101  nbuhgr  29803  nbuhgr2vtx1edgblem  29811  shex  31693  dfch2  31888  fpwrelmap  33204  xrsclat  33451  cmpcref  34360  sigaex  34620  sigaval  34621  insiga  34648  sigapisys  34666  sigaldsys  34670  measdivcst  34735  ballotlem2  35000  erdszelem7  35776  erdsze2lem2  35783  rellysconn  35830  neibastop2lem  36979  neibastop3  36981  topmeet  36983  topjoin  36984  neifg  36990  mh-infprim2bi  37166  bj-snglss  37714  bj-pw0ALT  37793  bj-restpw  37842  bj-imdirval2lem  37934  bj-imdiridlem  37937  dissneqlem  38094  topdifinfeq  38104  pibt2  38171  heibor1lem  38559  psubspset  40617  psubclsetN  40809  lcdlss  42492  ismrcd1  43543  pw2f1ocnv  43878  filnm  43931  hbtlem6  43970  dfno2  44268  elmapintrab  44416  clcnvlem  44463  psshepw  44628  ssclaxsep  45805  pwclaxpow  45807  sprsymrelfo  48397  uspgrsprfo  49064  setrec2fun  50618  setrecsres  50628