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 )