Definition df-pw 1799

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.

Assertion

Ref	Expression
df-pw	⊢ ℘A = {x∣x ⊆ A}

Distinct variable group(s):   x,A

Detailed syntax breakdown of Definition df-pw

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cpw 1798	. 2 class ℘A
3	vx	. . . . 5 set x
4	3	cv 1089	. . . 4 class x
5	4, 1	wss 1487	. . 3 wff x ⊆ A
6	5, 3	cab 1090	. 2 class {x∣x ⊆ A}
7	2, 6	wceq 1091	1 wff ℘A = {x∣x ⊆ A}

This definition is referenced by:  pweq 1800  elpw 1801  pwex 1806  snsspw 1857  pw0 1882  pwpw0 1883  iunpw 2040  mapex 3261  ssenen 3399  npex 3885  infmap2lem2 4952  gch-kn 4957  shex 5115

metamath.org