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