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 B A 𝒫 B

Proof

Step Hyp Ref Expression
1 snelpwg A B A B A 𝒫 B
2 1 ibi A B A 𝒫 B