Definition df-pw 2407

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 2406	. 2 class P~A
3		vx	. . . . 5 set x
4	3	cv 957	. . . 4 class x
5	4, 1	wss 2051	. . 3 wff x (_ A
6	5, 3	cab 1466	. 2 class {x | x (_ A}
7	2, 6	wceq 958	1 wff P~A = {x | x (_ A}

This definition is referenced by:  pweq 2408  elpw 2409  pw0 2473  pwpw0 2474  snsspw 2484  pwsn 2505  pwsnALT 2506  pwex 2752  iunpw 2921  orduniss2 3097  mapex 4335  mapsspw 4348  ssenen 4511  npex 5110  infmap2lem2 7589  gch-kn 7596  isbasis2g 7618  cncnplem1 7778  opnfss 7862  issubg 8119  avril1 8786  shex 9079

Copyright terms: Public domain