Theorem pw0

Description: Compute the power set of the empty set. Theorem 89 of Suppes p. 47. (Contributed by NM, 5-Aug-1993) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	pw0	|- ~P (/) = { (/) }

Proof

Step	Hyp	Ref	Expression
1		ss0b	|- ( x C_ (/) <-> x = (/) )
2	1	abbii	|- { x | x C_ (/) } = { x | x = (/) }
3		df-pw	|- ~P (/) = { x | x C_ (/) }
4		df-sn	|- { (/) } = { x | x = (/) }
5	2 3 4	3eqtr4i	|- ~P (/) = { (/) }