Theorem elpwg 2462

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

Assertion

Ref	Expression
elpwg	⊢ (A ∈ C → (A ∈ ℘B ↔ A ⊆ B))

Proof of Theorem elpwg

Step	Hyp	Ref	Expression
1		eleq1 1577	. . 3 ⊢ (x = A → (x ∈ ℘B ↔ A ∈ ℘B))
2		sseq1 2134	. . 3 ⊢ (x = A → (x ⊆ B ↔ A ⊆ B))
3	1, 2	bibi12d 632	. 2 ⊢ (x = A → ((x ∈ ℘B ↔ x ⊆ B) ↔ (A ∈ ℘B ↔ A ⊆ B)))
4		visset 1859	. . 3 ⊢ x ∈ V
5	4	elpw 2461	. 2 ⊢ (x ∈ ℘B ↔ x ⊆ B)
6	3, 5	vtoclg 1893	1 ⊢ (A ∈ C → (A ∈ ℘B ↔ A ⊆ B))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992   ∈ wcel 994   ⊆ wss 2099  ℘cpw 2458

This theorem is referenced by:  elpwi 2463  elpw2g 2801  axpweq 2817  pwel 2838  eldifpw 3133  elpwun 3134  elpwunsn 3135  r1rankid 4840  grothpw 9054  inpws1 10739  mapdiscn 11014  cnfilca 11088  compcov 11486  compsublem 11487  compfipin0lem 11492  compfipin0 11493  heiborlem1 12011

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105  df-pw 2459

Copyright terms: Public domain