Theorem velpw 4561

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  sspw  4567  pwv  4574  pwss  4581  snsspw  4798  pwpr  4827  pwtp  4828  pwuni  4905  sspwuni  5059  iinpw  5065  iunpwss  5066  ssextss  5420  pwin  5541  dffr6  5606  sorpsscmpl  7751  iunpw  7786  ordpwsuc  7827  fabexd  7950  abexssex  7983  qsss  8800  fsetsspwxp  8879  mapval2  8904  pmsspw  8909  uniixp  8953  fineqvlem  9261  fival  9408  hartogslem1  9540  setrec2fun  9977  tskwe  10035  cfval2  10342  cflim3  10344  cflim2  10345  cfslb  10348  compsscnvlem  10452  fin1a2lem13  10494  axdc3lem  10532  fpwwe2lem1  10720  fpwwe2lem10  10729  fpwwe2lem11  10730  fpwwe  10735  canthwe  10740  axgroth5  10913  axgroth6  10917  wuncn  11259  ishashinf  14612  vdwmc  17162  ramub2  17198  ram0  17206  restsspw  17608  ismred  17778  mremre  17780  acsfn  17839  submgmacs  18912  submacs  19029  subgacs  19377  nsgacs  19378  sylow2alem2  19838  sylow2a  19839  dprdres  20250  subgdmdprd  20256  pgpfac1lem5  20301  subrngmre  20820  subsubrng2  20822  subrgmre  20855  subsubrg2  20857  sdrgacs  21064  lssintcl  21245  lssmre  21247  lssacs  21248  cssmre  22005  istopon  23236  isbasis2g  23272  tgval2  23280  unitg  23291  distop  23319  cldss2  23354  ntreq0  23401  discld  23413  neisspw  23431  restdis  23502  cnntr  23599  isnrm2  23682  cmpcovf  23715  fincmp  23717  cmpsublem  23723  cmpsub  23724  cmpcld  23726  cmpfi  23732  is1stc2  23766  2ndcdisj  23781  llyi  23799  nllyi  23800  nlly2i  23801  llynlly  23802  subislly  23806  restnlly  23807  llyrest  23810  llyidm  23813  nllyidm  23814  islocfin  23842  ptuni2  23901  prdstopn  23953  qtoptop2  24024  qtopuni  24027  tgqtop  24037  isfbas2  24160  isfild  24183  elfg  24196  cfinfil  24218  csdfil  24219  supfil  24220  isufil2  24233  filssufilg  24236  uffix  24246  ufildr  24256  fin1aufil  24257  alexsubb  24371  alexsubALTlem1  24372  alexsubALTlem2  24373  alexsubALT  24376  ptcmplem5  24381  cldsubg  24436  ustfn  24527  ustfilxp  24538  ustn0  24546  dscopn  24898  voliunlem2  25878  vitali  25940  dmcuts  28183  madef  28228  nbuhgr  29930  nbuhgr2vtx1edgblem  29938  shex  31820  dfch2  32015  fpwrelmap  33372  xrsclat  33619  cmpcref  34529  sigaex  34789  sigaval  34790  insiga  34817  sigapisys  34835  sigaldsys  34839  measdivcst  34904  ballotlem2  35168  abweex  35770  erdszelem7  36049  erdsze2lem2  36056  rellysconn  36103  neibastop2lem  37241  neibastop3  37243  topmeet  37245  topjoin  37246  neifg  37252  mh-infprim2bi  37428  bj-snglss  37976  bj-pw0ALT  38057  bj-restpw  38106  bj-imdirval2lem  38197  bj-imdiridlem  38200  dissneqlem  38357  topdifinfeq  38367  pibt2  38434  heibor1lem  38837  psubspset  40895  psubclsetN  41087  lcdlss  42770  ismrcd1  43803  pw2f1ocnv  44138  filnm  44186  hbtlem6  44225  dfno2  44523  elmapintrab  44671  clcnvlem  44717  psshepw  44882  ssclaxsep  46066  pwclaxpow  46068  sprsymrelfo  48673  uspgrsprfo  49340  setrecsres  50964