![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-pw | 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 𝐴 is { 3 , 5 , 7 }, then 𝒫 𝐴 is { (/) , { 3 } , { 5 } , { 7 } , { 3 , 5 } , { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } }. We will later introduce the Axiom of Power Sets. Still later we will prove 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, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-pw | ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cpw 3590 | . 2 class 𝒫 𝐴 |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1363 | . . . 4 class 𝑥 |
5 | 4, 1 | wss 3144 | . . 3 wff 𝑥 ⊆ 𝐴 |
6 | 5, 3 | cab 2175 | . 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 2, 6 | wceq 1364 | 1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
Colors of variables: wff set class |
This definition is referenced by: pweq 3593 elpw 3596 nfpw 3603 pwss 3606 pw0 3754 snsspw 3779 pwsnss 3818 vpwex 4194 abssexg 4197 iunpw 4495 iotass 5210 mapex 6672 ssenen 6869 tgvalex 12734 bdcpw 15018 |
Copyright terms: Public domain | W3C validator |