Metamath Proof Explorer


Theorem snelpwi

Description: If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 snelpwg
 |-  ( A e. B -> ( A e. B <-> { A } e. ~P B ) )
2 1 ibi
 |-  ( A e. B -> { A } e. ~P B )