Theorem velpw 4578

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 4577	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2107   ⊆ wss 3924  𝒫 cpw 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-ss 3941  df-pw 4575

This theorem is referenced by:  sspw  4584  pwss  4596  snsspw  4817  pwpr  4874  pwtp  4875  pwv  4877  pwuni  4918  sspwuni  5073  iinpw  5079  iunpwss  5080  ssextss  5425  pwin  5541  dffr6  5606  sorpsscmpl  7722  iunpw  7759  ordpwsuc  7803  fabexd  7927  fabexgOLD  7929  abexssex  7963  qsss  8786  fsetsspwxp  8861  mapval2  8880  pmsspw  8885  uniixp  8929  fineqvlem  9264  fival  9418  hartogslem1  9548  tskwe  9956  cfval2  10266  cflim3  10268  cflim2  10269  cfslb  10272  compsscnvlem  10376  fin1a2lem13  10418  axdc3lem  10456  fpwwe2lem1  10637  fpwwe2lem10  10646  fpwwe2lem11  10647  fpwwe  10652  canthwe  10657  axgroth5  10830  axgroth6  10834  wuncn  11176  ishashinf  14469  vdwmc  16983  ramub2  17019  ram0  17027  restsspw  17430  ismred  17599  mremre  17601  acsfn  17656  submgmacs  18680  submacs  18790  subgacs  19129  nsgacs  19130  sylow2alem2  19584  sylow2a  19585  dprdres  19996  subgdmdprd  20002  pgpfac1lem5  20047  subrngmre  20507  subsubrng2  20509  subrgmre  20542  subsubrg2  20544  sdrgacs  20746  lssintcl  20906  lssmre  20908  lssacs  20909  cssmre  21638  istopon  22835  isbasis2g  22871  tgval2  22879  unitg  22890  distop  22918  cldss2  22953  ntreq0  23000  discld  23012  neisspw  23030  restdis  23101  cnntr  23198  isnrm2  23281  cmpcovf  23314  fincmp  23316  cmpsublem  23322  cmpsub  23323  cmpcld  23325  cmpfi  23331  is1stc2  23365  2ndcdisj  23379  llyi  23397  nllyi  23398  nlly2i  23399  llynlly  23400  subislly  23404  restnlly  23405  llyrest  23408  llyidm  23411  nllyidm  23412  islocfin  23440  ptuni2  23499  prdstopn  23551  qtoptop2  23622  qtopuni  23625  tgqtop  23635  isfbas2  23758  isfild  23781  elfg  23794  cfinfil  23816  csdfil  23817  supfil  23818  isufil2  23831  filssufilg  23834  uffix  23844  ufildr  23854  fin1aufil  23855  alexsubb  23969  alexsubALTlem1  23970  alexsubALTlem2  23971  alexsubALT  23974  ptcmplem5  23979  cldsubg  24034  ustfn  24125  ustfilxp  24136  ustn0  24144  dscopn  24497  voliunlem2  25489  vitali  25551  dmscut  27759  madef  27798  nbuhgr  29254  nbuhgr2vtx1edgblem  29262  shex  31125  dfch2  31320  fpwrelmap  32645  xrsclat  32922  cmpcref  33789  sigaex  34049  sigaval  34050  insiga  34076  sigapisys  34094  sigaldsys  34098  measdivcst  34163  ballotlem2  34429  erdszelem7  35140  erdsze2lem2  35147  rellysconn  35194  dffr5  35692  neibastop2lem  36299  neibastop3  36301  topmeet  36303  topjoin  36304  neifg  36310  bj-snglss  36909  bj-pw0ALT  36988  bj-restpw  37031  bj-imdirval2lem  37121  bj-imdiridlem  37124  dissneqlem  37279  topdifinfeq  37289  pibt2  37356  heibor1lem  37754  psubspset  39684  psubclsetN  39876  lcdlss  41559  ismrcd1  42646  pw2f1ocnv  42986  filnm  43039  hbtlem6  43078  dfno2  43377  elmapintrab  43525  clcnvlem  43572  psshepw  43737  ssclaxsep  44934  pwclaxpow  44936  sprsymrelfo  47429  uspgrsprfo  48009  setrec2fun  49276  setrecsres  49286