Definition df-pw 2459

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 2458	. 2 class P~A
3		vx	. . . . 5 set x
4	3	cv 991	. . . 4 class x
5	4, 1	wss 2099	. . 3 wff x (_ A
6	5, 3	cab 1505	. 2 class {x | x (_ A}
7	2, 6	wceq 992	1 wff P~A = {x | x (_ A}

This definition is referenced by:  pweq 2460  elpw 2461  pwss 2466  pw0 2532  pwpw0 2533  snsspw 2544  pwsn 2565  pwsnALT 2566  pwpr 2567  pwex 2823  iunpw 3137  orduniss2 3187  mapex 4469  mapsspw 4482  ssenen 4651  npex 5245  infmap2lem2 7792  gch-kn 7799  isbasis2g 7824  cncnplem1 7984  opnfss 8068  issubg 8358  grothpw 9054  avril1 9058  shex 9353  neibastop2lem1 11580  neibastop2lem4 11583  topjoin 11588  fipreima 11848

Copyright terms: Public domain