Definition df-pw 2399

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	|- P~A = {x | x (_ A}

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-pw

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cpw 2398	. 2 class P~A
3		vx	. . . . 5 set x
4	3	cv 954	. . . 4 class x
5	4, 1	wss 2044	. . 3 wff x (_ A
6	5, 3	cab 1462	. 2 class {x | x (_ A}
7	2, 6	wceq 955	1 wff P~A = {x | x (_ A}

This definition is referenced by:  pweq 2400  elpw 2401  pw0 2465  pwpw0 2466  snsspw 2476  pwsn 2497  pwex 2741  iunpw 2910  orduniss2 3086  mapex 4321  mapsspw 4334  ssenen 4493  npex 5074  infmap2lem2 7540  gch-kn 7547  isbasis2g 7572  cncnplem1 7734  opnfss 7820  issubg 8080  avril1 8739  shex 9032

Copyright terms: Public domain