Theorem elpw 1801

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47.

Hypothesis

Ref	Expression
elpw.1	⊢ A ∈ V

Assertion

Ref	Expression
elpw	⊢ (A ∈ ℘B ↔ A ⊆ B)

Proof of Theorem elpw

Step	Hyp	Ref	Expression
1		elpw.1	. 2 ⊢ A ∈ V
2		eleq1 1149	. 2 ⊢ (x = A → (x ∈ ℘B ↔ A ∈ ℘B))
3		sseq1 1521	. 2 ⊢ (x = A → (x ⊆ B ↔ A ⊆ B))
4		df-pw 1799	. . 3 ⊢ ℘B = {x∣x ⊆ B}
5	4	cleqabi 1176	. 2 ⊢ (x ∈ ℘B ↔ x ⊆ B)
6	1, 2, 3, 5	vtoclb 1381	1 ⊢ (A ∈ ℘B ↔ A ⊆ B)

Syntax hints:   ↔ wb 127   ∈ wcel 1092  Vcvv 1348   ⊆ wss 1487  ℘cpw 1798

This theorem is referenced by:  elpwg 1802  hbpw 1804  pwid 1805  prsspw 1858  snelpw 1861  sspwb 1863  ssextss 1864  pwv 1884  pwin 1915  pwunss 1916  pwssun 1917  unipw 1960  pwuni 1961  iinpw 2038  iunpwss 2039  iunpw 2040  dftr4 2046  onpwsuc 2315  xpex 2488  canth 2945  pw2en 3348  ssenen 3399  inf3lem6 3469  setind2 3493  r1tr 3498  tz9.12lem3 3505  rankel 3524  rankval3 3525  rankpw 3528  numthlem 3598  infxpidmlem9 4941  infmap2lem2 4952  ocvalt 5161  spanvalt 5300  hsupval2t 5301  sshjvalt 5321  sshjval3t 5327

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492  df-pw 1799

metamath.org