![]() |
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 30176). We will later introduce the Axiom of Power Sets ax-pow 5354, which can be expressed in class notation per pwexg 5367. Still later we will prove, in hashpw 14397, 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 4595 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1532 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3941 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2701 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1533 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: elpwg 4598 pweqALT 4610 nfpw 4614 pw0 4808 pwpw0 4809 pwsn 4893 vpwex 5366 abssexg 5371 orduniss2 7815 mapex 8823 ssenen 9148 domtriomlem 10434 npex 10978 ustval 24051 avril1 30210 fineqvpow 34614 dfon2lem2 35278 bj-velpwALT 36434 |
Copyright terms: Public domain | W3C validator |