![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-pw | Structured version Visualization version GIF version |
Description: Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if 𝐴 = {3, 5, 7}, then 𝒫 𝐴 = {∅, {3}, {5}, {7}, {3, 5}, {3, 7}, {5, 7}, {3, 5, 7}} (ex-pw 27845). We will later introduce the Axiom of Power Sets ax-pow 5066, which can be expressed in class notation per pwexg 5079. Still later we will prove, in hashpw 13513, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.) |
Ref | Expression |
---|---|
df-pw | ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cpw 4379 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1657 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3799 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2812 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1658 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: pweq 4382 elpw 4385 nfpw 4393 pw0 4562 pwpw0 4563 pwsn 4651 pwsnALT 4652 vpwex 5078 abssexg 5082 orduniss2 7295 mapex 8129 ssenen 8404 domtriomlem 9580 npex 10124 ustval 22377 avril1 27878 dfon2lem2 32228 |
Copyright terms: Public domain | W3C validator |