Definition df-pw 4605

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 30238). We will later introduce the Axiom of Power Sets ax-pow 5365, which can be expressed in class notation per pwexg 5378. Still later we will prove, in hashpw 14427, 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.)

Assertion

Ref	Expression
df-pw	⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-pw

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cpw 4603	. 2 class 𝒫 𝐴
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1533	. . . 4 class 𝑥
5	4, 1	wss 3947	. . 3 wff 𝑥 ⊆ 𝐴
6	5, 3	cab 2705	. 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴}
7	2, 6	wceq 1534	1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}

This definition is referenced by:  elpwg  4606  pweqALT  4618  nfpw  4622  pw0  4816  pwpw0  4817  pwsn  4901  vpwex  5377  abssexg  5382  orduniss2  7836  mapex  8850  ssenen  9175  domtriomlem  10465  npex  11009  ustval  24106  avril1  30272  fineqvpow  34716  dfon2lem2  35380  bj-velpwALT  36532