Metamath Proof Explorer

Theorem snelpwi

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011)

Ref Expression
Assertion snelpwi 
|- ( A e. B -> { A } e. ~P B )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. B -> { A } C_ B )
2 snex 
 |-  { A } e. _V
3 2 elpw 
 |-  ( { A } e. ~P B <-> { A } C_ B )
4 1 3 sylibr 
 |-  ( A e. B -> { A } e. ~P B )