Definition df-pw 4552

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 30404). We will later introduce the Axiom of Power Sets ax-pow 5303, which can be expressed in class notation per pwexg 5316. Still later we will prove, in hashpw 14340, 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 4550	. 2 class 𝒫 𝐴
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1540	. . . 4 class 𝑥
5	4, 1	wss 3902	. . 3 wff 𝑥 ⊆ 𝐴
6	5, 3	cab 2709	. 2 class {𝑥 ∣ 𝑥 ⊆ 𝐴}
7	2, 6	wceq 1541	1 wff 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}

This definition is referenced by:  elpwg  4553  pweqALT  4565  nfpw  4569  pw0  4764  pwpw0  4765  pwsn  4852  vpwex  5315  abssexg  5320  orduniss2  7763  mapexOLD  8756  ssenen  9064  domtriomlem  10330  npex  10874  ustval  24116  avril1  30438  fineqvpow  35126  dfon2lem2  35817  bj-velpwALT  37086