Definition df-pw 3035

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	|- ~PA = {x | x C_ 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 3032	. 2 class ~PA
3		vx	. . . . 5 set x
4	3	cv 1297	. . . 4 class x
5	4, 1	wss 2593	. . 3 wff x C_ A
6	5, 3	cab 1871	. 2 class {x | x C_ A}
7	2, 6	wceq 1298	1 wff ~PA = {x | x C_ A}

This definition is referenced by:  pweq 3036  elpw 3037  pwss 3043  pw0 3132  pw0OLD 3133  pwpw0 3134  snsspw 3149  pwsn 3172  pwsnALT 3173  pwpr 3174  pwex 3487  pwexOLD 3488  abssexg 3490  iunpw 3858  orduniss2 3913  mapex 5387  mapsspw 5400  ssenen 5598  npex 6243  infmap2lem2 8849  gch-kn 8856  isbasis2g 8881  cncnplem1 9051  opnfss 9135  issubg 9425  grothpw 10134  avril1 10142  fipreima 10175  shex 10710  dfon2lem2 13850  dford4lem1 13859  neibastop2lem1 15519  neibastop2lem4 15522  topjoin 15527  fipreimaOLD 15756  psubspset 17225  psubclset 17346

Copyright terms: Public domain