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 | ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssi | ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 ) | |
2 | snex | ⊢ { 𝐴 } ∈ V | |
3 | 2 | elpw | ⊢ ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) |
4 | 1 3 | sylibr | ⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ∈ 𝒫 𝐵 ) |