Metamath Proof Explorer

Theorem snsspw

Description: The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion snsspw 
|- { A } C_ ~P A

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( x = A -> x C_ A )
2 velsn 
 |-  ( x e. { A } <-> x = A )
3 velpw 
 |-  ( x e. ~P A <-> x C_ A )
4 1 2 3 3imtr4i 
 |-  ( x e. { A } -> x e. ~P A )
5 4 ssriv 
 |-  { A } C_ ~P A