Definition df-pw1 4138

Description: Define unit power class. Definition from [Rosser] p. 252. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-pw1	|- ~P1 A = (~PA i^i 1c)

Detailed syntax breakdown of Definition df-pw1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cpw1 4136	. 2 class ~P1 A
3	1	cpw 3723	. . 3 class ~PA
4		c1c 4135	. . 3 class 1c
5	3, 4	cin 3209	. 2 class (~PA i^i 1c)
6	2, 5	wceq 1642	1 wff ~P1 A = (~PA i^i 1c)

This definition is referenced by:  pw1eq  4144  elpw1  4145  pw1ss1c  4159  pw10  4162  pw1ss  4170  pw1sspw  4172