Theorem velpw 4580

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-pw 4577

This theorem is referenced by:  sspw  4586  pwss  4598  snsspw  4820  pwpr  4877  pwtp  4878  pwv  4880  pwuni  4921  sspwuni  5076  iinpw  5082  iunpwss  5083  ssextss  5428  pwin  5544  dffr6  5609  sorpsscmpl  7726  iunpw  7763  ordpwsuc  7807  fabexd  7931  fabexgOLD  7933  abexssex  7967  qsss  8790  fsetsspwxp  8865  mapval2  8884  pmsspw  8889  uniixp  8933  fineqvlem  9268  fival  9422  hartogslem1  9554  tskwe  9962  cfval2  10272  cflim3  10274  cflim2  10275  cfslb  10278  compsscnvlem  10382  fin1a2lem13  10424  axdc3lem  10462  fpwwe2lem1  10643  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe  10658  canthwe  10663  axgroth5  10836  axgroth6  10840  wuncn  11182  ishashinf  14479  vdwmc  16996  ramub2  17032  ram0  17040  restsspw  17443  ismred  17612  mremre  17614  acsfn  17669  submgmacs  18693  submacs  18803  subgacs  19142  nsgacs  19143  sylow2alem2  19597  sylow2a  19598  dprdres  20009  subgdmdprd  20015  pgpfac1lem5  20060  subrngmre  20520  subsubrng2  20522  subrgmre  20555  subsubrg2  20557  sdrgacs  20759  lssintcl  20919  lssmre  20921  lssacs  20922  cssmre  21651  istopon  22848  isbasis2g  22884  tgval2  22892  unitg  22903  distop  22931  cldss2  22966  ntreq0  23013  discld  23025  neisspw  23043  restdis  23114  cnntr  23211  isnrm2  23294  cmpcovf  23327  fincmp  23329  cmpsublem  23335  cmpsub  23336  cmpcld  23338  cmpfi  23344  is1stc2  23378  2ndcdisj  23392  llyi  23410  nllyi  23411  nlly2i  23412  llynlly  23413  subislly  23417  restnlly  23418  llyrest  23421  llyidm  23424  nllyidm  23425  islocfin  23453  ptuni2  23512  prdstopn  23564  qtoptop2  23635  qtopuni  23638  tgqtop  23648  isfbas2  23771  isfild  23794  elfg  23807  cfinfil  23829  csdfil  23830  supfil  23831  isufil2  23844  filssufilg  23847  uffix  23857  ufildr  23867  fin1aufil  23868  alexsubb  23982  alexsubALTlem1  23983  alexsubALTlem2  23984  alexsubALT  23987  ptcmplem5  23992  cldsubg  24047  ustfn  24138  ustfilxp  24149  ustn0  24157  dscopn  24510  voliunlem2  25502  vitali  25564  dmscut  27773  madef  27812  nbuhgr  29268  nbuhgr2vtx1edgblem  29276  shex  31139  dfch2  31334  fpwrelmap  32656  xrsclat  32949  cmpcref  33827  sigaex  34087  sigaval  34088  insiga  34114  sigapisys  34132  sigaldsys  34136  measdivcst  34201  ballotlem2  34467  erdszelem7  35165  erdsze2lem2  35172  rellysconn  35219  dffr5  35717  neibastop2lem  36324  neibastop3  36326  topmeet  36328  topjoin  36329  neifg  36335  bj-snglss  36934  bj-pw0ALT  37013  bj-restpw  37056  bj-imdirval2lem  37146  bj-imdiridlem  37149  dissneqlem  37304  topdifinfeq  37314  pibt2  37381  heibor1lem  37779  psubspset  39709  psubclsetN  39901  lcdlss  41584  ismrcd1  42668  pw2f1ocnv  43008  filnm  43061  hbtlem6  43100  dfno2  43399  elmapintrab  43547  clcnvlem  43594  psshepw  43759  ssclaxsep  44955  pwclaxpow  44957  sprsymrelfo  47459  uspgrsprfo  48071  setrec2fun  49504  setrecsres  49514