Metamath Proof Explorer


Theorem 0elpw

Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007)

Ref Expression
Assertion 0elpw
|- (/) e. ~P A

Proof

Step Hyp Ref Expression
1 0ss
 |-  (/) C_ A
2 0ex
 |-  (/) e. _V
3 2 elpw
 |-  ( (/) e. ~P A <-> (/) C_ A )
4 1 3 mpbir
 |-  (/) e. ~P A