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 28136). We will later introduce the Axiom of Power Sets ax-pow 5258, which can be expressed in class notation per pwexg 5271. Still later we will prove, in hashpw 13787, 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 4537 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1527 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3935 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2799 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1528 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: pweq 4540 elpwg 4543 elpwOLD 4546 nfpw 4553 pw0 4739 pwpw0 4740 pwsn 4824 pwsnALT 4825 vpwex 5270 abssexg 5274 orduniss2 7536 mapex 8402 ssenen 8680 domtriomlem 9853 npex 10397 ustval 22740 avril1 28170 dfon2lem2 32927 |
Copyright terms: Public domain | W3C validator |