Metamath Proof Explorer


Theorem pwne0

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

Ref Expression
Assertion pwne0
|- ~P A =/= (/)

Proof

Step Hyp Ref Expression
1 0elpw
 |-  (/) e. ~P A
2 1 ne0ii
 |-  ~P A =/= (/)