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 =/= (/)