Theorem pwne0

Description: A power class is never empty. (Contributed by NM, 3-Sep-2018)

	Ref	Expression
Assertion	pwne0	⊢ 𝒫 𝐴 ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		0elpw	⊢ ∅ ∈ 𝒫 𝐴
2	1	ne0ii	⊢ 𝒫 𝐴 ≠ ∅