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 28208). We will later introduce the Axiom of Power Sets ax-pow 5266, which can be expressed in class notation per pwexg 5279. Still later we will prove, in hashpw 13798, 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 4539 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1536 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3936 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2799 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1537 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: elpwg 4542 elpwOLD 4545 pweqALT 4556 nfpw 4560 pw0 4745 pwpw0 4746 pwsn 4830 pwsnOLD 4831 vpwex 5278 abssexg 5283 orduniss2 7548 mapex 8412 ssenen 8691 domtriomlem 9864 npex 10408 ustval 22811 avril1 28242 dfon2lem2 33029 |
Copyright terms: Public domain | W3C validator |