Theorem pwsn

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

	Ref	Expression
Assertion	pwsn	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }

Proof

Step	Hyp	Ref	Expression
1		sssn	⊢ ( 𝑥 ⊆ { 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) )
2	1	abbii	⊢ { 𝑥 ∣ 𝑥 ⊆ { 𝐴 } } = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) }
3		df-pw	⊢ 𝒫 { 𝐴 } = { 𝑥 ∣ 𝑥 ⊆ { 𝐴 } }
4		dfpr2	⊢ { ∅ , { 𝐴 } } = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) }
5	2 3 4	3eqtr4i	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }