Theorem velpw 3573

Description: Setvar variable membership in a power class (common case). See elpw 3572. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
velpw	⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem velpw

Step	Hyp	Ref	Expression
1		vex 2733	. 2 ⊢ 𝑥 ∈ V
2	1	elpw 3572	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 104   ∈ wcel 2141   ⊆ wss 3121  𝒫 cpw 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134  df-pw 3568

This theorem is referenced by:  ordpwsucss  4551  fabexg  5385  abexssex  6104  qsss  6572  mapval2  6656  pmsspw  6661  uniixp  6699  exmidpw  6886  exmidpweq  6887  pw1fin  6888  pw1dc0el  6889  fival  6947  npsspw  7433  restsspw  12589  istopon  12805  isbasis2g  12837  tgval2  12845  unitg  12856  distop  12879  cldss2  12900  ntreq0  12926  discld  12930  neisspw  12942  restdis  12978  cnntr  13019