Metamath Proof Explorer


Theorem snelpw

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998)

Ref Expression
Hypothesis snelpw.1
|- A e. _V
Assertion snelpw
|- ( A e. B <-> { A } e. ~P B )

Proof

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