Metamath Proof Explorer


Theorem snelpw

Description: A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998)

Ref Expression
Hypothesis snelpw.ex A V
Assertion snelpw A B A 𝒫 B

Proof

Step Hyp Ref Expression
1 snelpw.ex A V
2 snelpwg A V A B A 𝒫 B
3 1 2 ax-mp A B A 𝒫 B