Theorem pwsn

Description: The power set of a singleton. (Contributed by NM, 5-Jun-2006)

	Ref	Expression
Assertion	pwsn	|- ~P { A } = { (/) , { A } }

Proof

Step	Hyp	Ref	Expression
1		sssn	|- ( x C_ { A } <-> ( x = (/) \/ x = { A } ) )
2	1	abbii	|- { x | x C_ { A } } = { x | ( x = (/) \/ x = { A } ) }
3		df-pw	|- ~P { A } = { x | x C_ { A } }
4		dfpr2	|- { (/) , { A } } = { x | ( x = (/) \/ x = { A } ) }
5	2 3 4	3eqtr4i	|- ~P { A } = { (/) , { A } }