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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146   ⊆ wss 3906  𝒫 cpw 4564

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-pw 4566

This theorem is used by:  sspw  4575  pwss  4588  snsspw  4811  pwpr  4868  pwtp  4869  pwv  4871  pwuni  4913  sspwuni  5068  iinpw  5074  iunpwss  5075  ssextss  5436  pwin  5554  dffr6  5619  sorpsscmpl  7737  iunpw  7772  ordpwsuc  7813  fabexd  7936  abexssex  7969  qsss  8775  fsetsspwxp  8852  mapval2  8872  pmsspw  8877  uniixp  8921  fineqvlem  9229  fival  9375  hartogslem1  9507  tskwe  9948  cfval2  10255  cflim3  10257  cflim2  10258  cfslb  10261  compsscnvlem  10365  fin1a2lem13  10407  axdc3lem  10445  fpwwe2lem1  10627  fpwwe2lem10  10636  fpwwe2lem11  10637  fpwwe  10642  canthwe  10647  axgroth5  10820  axgroth6  10824  wuncn  11166  ishashinf  14513  vdwmc  17055  ramub2  17091  ram0  17099  restsspw  17501  ismred  17671  mremre  17673  acsfn  17732  submgmacs  18796  submacs  18909  subgacs  19250  nsgacs  19251  sylow2alem2  19711  sylow2a  19712  dprdres  20123  subgdmdprd  20129  pgpfac1lem5  20174  subrngmre  20690  subsubrng2  20692  subrgmre  20725  subsubrg2  20727  sdrgacs  20933  lssintcl  21114  lssmre  21116  lssacs  21117  cssmre  21872  istopon  23098  isbasis2g  23134  tgval2  23142  unitg  23153  distop  23181  cldss2  23216  ntreq0  23263  discld  23275  neisspw  23293  restdis  23364  cnntr  23461  isnrm2  23544  cmpcovf  23577  fincmp  23579  cmpsublem  23585  cmpsub  23586  cmpcld  23588  cmpfi  23594  is1stc2  23628  2ndcdisj  23642  llyi  23660  nllyi  23661  nlly2i  23662  llynlly  23663  subislly  23667  restnlly  23668  llyrest  23671  llyidm  23674  nllyidm  23675  islocfin  23703  ptuni2  23762  prdstopn  23814  qtoptop2  23885  qtopuni  23888  tgqtop  23898  isfbas2  24021  isfild  24044  elfg  24057  cfinfil  24079  csdfil  24080  supfil  24081  isufil2  24094  filssufilg  24097  uffix  24107  ufildr  24117  fin1aufil  24118  alexsubb  24232  alexsubALTlem1  24233  alexsubALTlem2  24234  alexsubALT  24237  ptcmplem5  24242  cldsubg  24297  ustfn  24388  ustfilxp  24399  ustn0  24407  dscopn  24759  voliunlem2  25739  vitali  25801  dmcuts  28013  madef  28058  nbuhgr  29722  nbuhgr2vtx1edgblem  29730  shex  31593  dfch2  31788  fpwrelmap  33107  xrsclat  33354  cmpcref  34263  sigaex  34523  sigaval  34524  insiga  34551  sigapisys  34569  sigaldsys  34573  measdivcst  34638  ballotlem2  34903  erdszelem7  35702  erdsze2lem2  35709  rellysconn  35756  dffr5  36259  neibastop2lem  36904  neibastop3  36906  topmeet  36908  topjoin  36909  neifg  36915  mh-infprim2bi  37091  bj-snglss  37639  bj-pw0ALT  37718  bj-restpw  37767  bj-imdirval2lem  37859  bj-imdiridlem  37862  dissneqlem  38019  topdifinfeq  38029  pibt2  38096  heibor1lem  38493  psubspset  40551  psubclsetN  40743  lcdlss  42426  ismrcd1  43462  pw2f1ocnv  43797  filnm  43850  hbtlem6  43889  dfno2  44187  elmapintrab  44335  clcnvlem  44382  psshepw  44547  ssclaxsep  45724  pwclaxpow  45726  sprsymrelfo  48279  uspgrsprfo  48946  setrec2fun  50503  setrecsres  50513