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 28466). We will later introduce the Axiom of Power Sets ax-pow 5243, which can be expressed in class notation per pwexg 5256. Still later we will prove, in hashpw 13968, 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 4499 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1542 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3853 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2714 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1543 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: elpwg 4502 elpwOLD 4505 pweqALT 4516 nfpw 4520 pw0 4711 pwpw0 4712 pwsn 4797 pwsnOLD 4798 vpwex 5255 abssexg 5260 orduniss2 7590 mapex 8492 ssenen 8798 domtriomlem 10021 npex 10565 ustval 23054 avril1 28500 fineqvpow 32732 dfon2lem2 33430 |
Copyright terms: Public domain | W3C validator |