Theorem velpw 4544

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114   ⊆ wss 3936  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  elpwgOLD  4546  sspw  4552  pwss  4564  snsspw  4775  pwpr  4832  pwtp  4833  pwv  4835  pwuni  4875  sspwuni  5022  iinpw  5028  iunpwss  5029  ssextss  5346  pwin  5454  pwunssOLD  5455  sorpsscmpl  7460  iunpw  7493  ordpwsuc  7530  fabexg  7639  abexssex  7671  qsss  8358  mapval2  8436  pmsspw  8441  uniixp  8485  fineqvlem  8732  fival  8876  hartogslem1  9006  tskwe  9379  cfval2  9682  cflim3  9684  cflim2  9685  cfslb  9688  compsscnvlem  9792  fin1a2lem13  9834  axdc3lem  9872  fpwwe2lem1  10053  fpwwe2lem11  10062  fpwwe2lem12  10063  fpwwe  10068  canthwe  10073  axgroth5  10246  axgroth6  10250  wuncn  10592  ishashinf  13822  vdwmc  16314  ramub2  16350  ram0  16358  restsspw  16705  ismred  16873  mremre  16875  acsfn  16930  submacs  17991  subgacs  18313  nsgacs  18314  sylow2alem2  18743  sylow2a  18744  dprdres  19150  subgdmdprd  19156  pgpfac1lem5  19201  subrgmre  19559  subsubrg2  19562  sdrgacs  19580  lssintcl  19736  lssmre  19738  lssacs  19739  cssmre  20837  istopon  21520  isbasis2g  21556  tgval2  21564  unitg  21575  distop  21603  cldss2  21638  ntreq0  21685  discld  21697  neisspw  21715  restdis  21786  cnntr  21883  isnrm2  21966  cmpcovf  21999  fincmp  22001  cmpsublem  22007  cmpsub  22008  cmpcld  22010  cmpfi  22016  is1stc2  22050  2ndcdisj  22064  llyi  22082  nllyi  22083  nlly2i  22084  llynlly  22085  subislly  22089  restnlly  22090  llyrest  22093  llyidm  22096  nllyidm  22097  islocfin  22125  ptuni2  22184  prdstopn  22236  qtoptop2  22307  qtopuni  22310  tgqtop  22320  isfbas2  22443  isfild  22466  elfg  22479  cfinfil  22501  csdfil  22502  supfil  22503  isufil2  22516  filssufilg  22519  uffix  22529  ufildr  22539  fin1aufil  22540  alexsubb  22654  alexsubALTlem1  22655  alexsubALTlem2  22656  alexsubALT  22659  ptcmplem5  22664  cldsubg  22719  ustfn  22810  ustfilxp  22821  ustn0  22829  dscopn  23183  voliunlem2  24152  vitali  24214  nbuhgr  27125  nbuhgr2vtx1edgblem  27133  shex  28989  dfch2  29184  fpwrelmap  30469  xrsclat  30667  cmpcref  31114  sigaex  31369  sigaval  31370  insiga  31396  sigapisys  31414  sigaldsys  31418  measdivcst  31483  ballotlem2  31746  erdszelem7  32444  erdsze2lem2  32451  rellysconn  32498  dffr5  32989  dmscut  33272  neibastop2lem  33708  neibastop3  33710  topmeet  33712  topjoin  33713  neifg  33719  bj-snglss  34285  bj-pw0ALT  34345  bj-restpw  34386  bj-imdirval2  34476  bj-imdirid  34478  dissneqlem  34624  topdifinfeq  34634  pibt2  34701  heibor1lem  35102  psubspset  36895  psubclsetN  37087  lcdlss  38770  ismrcd1  39344  pw2f1ocnv  39683  filnm  39739  hbtlem6  39778  elmapintrab  39985  clcnvlem  40032  psshepw  40183  sprsymrelfo  43708  uspgrsprfo  44072  submgmacs  44120  setrec2fun  44844  setrecsres  44853