Theorem selpw 3442

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem selpw

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

Syntax hints:   ↔ wb 104   ∈ wcel 1439   ⊆ wss 3002  𝒫 cpw 3435

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2624  df-in 3008  df-ss 3015  df-pw 3437

This theorem is referenced by:  ordpwsucss  4398  fabexg  5213  abexssex  5912  qsss  6367  mapval2  6451  pmsspw  6456  uniixp  6494  exmidpw  6680  npsspw  7093  restsspw  11725  istopon  11775  isbasis2g  11806  tgval2  11814  unitg  11825  distop  11848  cldss2  11869  ntreq0  11895  discld  11899  neisspw  11911