Metamath Proof Explorer


Theorem snelpwi

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011)

Ref Expression
Assertion snelpwi ( 𝐴𝐵 → { 𝐴 } ∈ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 snssi ( 𝐴𝐵 → { 𝐴 } ⊆ 𝐵 )
2 snex { 𝐴 } ∈ V
3 2 elpw ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 )
4 1 3 sylibr ( 𝐴𝐵 → { 𝐴 } ∈ 𝒫 𝐵 )