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 | ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snelpwg | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ∈ 𝒫 𝐵 ) ) | |
2 | 1 | ibi | ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 ) |