This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snsspw

Description: The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion snsspw ⊢ A ⊆ 𝒫 A

Proof

Step Hyp Ref Expression
1 eqimss ⊢ x = A → x ⊆ A
2 velsn ⊢ x ∈ A ↔ x = A
3 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
4 1 2 3 3imtr4i ⊢ x ∈ A → x ∈ 𝒫 A
5 4 ssriv ⊢ A ⊆ 𝒫 A