Theorem pwne0

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

	Ref	Expression
Assertion	pwne0	$$⊢𝒫A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0elpw	$$⊢\varnothing \in 𝒫A$$
2	1	ne0ii	$$⊢𝒫A\ne \varnothing$$