Definition df-pw 4562

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 30895). We will later introduce the Axiom of Power Sets ax-pow 5334, which can be expressed in class notation per pwexg 5347. Still later we will prove, in hashpw 14503, 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 4560	. 2 class 𝒫 𝐴
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1569	. . . 4 class 𝑥
5	4, 1	wss 3902	. . 3 wff 𝑥 ⊆ 𝐴
6	5, 3	cab 2740	. 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴}
7	2, 6	wceq 1570	1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}

This definition is used by:  elpwg  4563  pweqALT  4575  nfpw  4579  pw0  4776  pwpw0  4777  pwsn  4863  vpwex  5346  abssexg  5351  orduniss2  7832  ssenen  9152  domtriomlem  10447  npex  10998  ustval  24430  avril1  30929  fineqvpow  35628  dfon2lem2  36348  bj-velpwALT  37784