Theorem velpw 4558

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-pw 4555

This theorem is referenced by:  sspw  4564  pwss  4576  snsspw  4798  pwpr  4855  pwtp  4856  pwv  4858  pwuni  4898  sspwuni  5052  iinpw  5058  iunpwss  5059  ssextss  5400  pwin  5514  dffr6  5579  sorpsscmpl  7674  iunpw  7711  ordpwsuc  7754  fabexd  7877  fabexgOLD  7879  abexssex  7912  qsss  8710  fsetsspwxp  8787  mapval2  8806  pmsspw  8811  uniixp  8855  fineqvlem  9167  fival  9321  hartogslem1  9453  tskwe  9865  cfval2  10173  cflim3  10175  cflim2  10176  cfslb  10179  compsscnvlem  10283  fin1a2lem13  10325  axdc3lem  10363  fpwwe2lem1  10544  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe  10559  canthwe  10564  axgroth5  10737  axgroth6  10741  wuncn  11083  ishashinf  14388  vdwmc  16908  ramub2  16944  ram0  16952  restsspw  17353  ismred  17522  mremre  17524  acsfn  17583  submgmacs  18609  submacs  18719  subgacs  19058  nsgacs  19059  sylow2alem2  19515  sylow2a  19516  dprdres  19927  subgdmdprd  19933  pgpfac1lem5  19978  subrngmre  20465  subsubrng2  20467  subrgmre  20500  subsubrg2  20502  sdrgacs  20704  lssintcl  20885  lssmre  20887  lssacs  20888  cssmre  21618  istopon  22815  isbasis2g  22851  tgval2  22859  unitg  22870  distop  22898  cldss2  22933  ntreq0  22980  discld  22992  neisspw  23010  restdis  23081  cnntr  23178  isnrm2  23261  cmpcovf  23294  fincmp  23296  cmpsublem  23302  cmpsub  23303  cmpcld  23305  cmpfi  23311  is1stc2  23345  2ndcdisj  23359  llyi  23377  nllyi  23378  nlly2i  23379  llynlly  23380  subislly  23384  restnlly  23385  llyrest  23388  llyidm  23391  nllyidm  23392  islocfin  23420  ptuni2  23479  prdstopn  23531  qtoptop2  23602  qtopuni  23605  tgqtop  23615  isfbas2  23738  isfild  23761  elfg  23774  cfinfil  23796  csdfil  23797  supfil  23798  isufil2  23811  filssufilg  23814  uffix  23824  ufildr  23834  fin1aufil  23835  alexsubb  23949  alexsubALTlem1  23950  alexsubALTlem2  23951  alexsubALT  23954  ptcmplem5  23959  cldsubg  24014  ustfn  24105  ustfilxp  24116  ustn0  24124  dscopn  24477  voliunlem2  25468  vitali  25530  dmscut  27740  madef  27784  nbuhgr  29306  nbuhgr2vtx1edgblem  29314  shex  31174  dfch2  31369  fpwrelmap  32689  xrsclat  32978  cmpcref  33819  sigaex  34079  sigaval  34080  insiga  34106  sigapisys  34124  sigaldsys  34128  measdivcst  34193  ballotlem2  34459  erdszelem7  35172  erdsze2lem2  35179  rellysconn  35226  dffr5  35729  neibastop2lem  36336  neibastop3  36338  topmeet  36340  topjoin  36341  neifg  36347  bj-snglss  36946  bj-pw0ALT  37025  bj-restpw  37068  bj-imdirval2lem  37158  bj-imdiridlem  37161  dissneqlem  37316  topdifinfeq  37326  pibt2  37393  heibor1lem  37791  psubspset  39726  psubclsetN  39918  lcdlss  41601  ismrcd1  42674  pw2f1ocnv  43013  filnm  43066  hbtlem6  43105  dfno2  43404  elmapintrab  43552  clcnvlem  43599  psshepw  43764  ssclaxsep  44959  pwclaxpow  44961  sprsymrelfo  47485  uspgrsprfo  48136  setrec2fun  49681  setrecsres  49691