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	⊢ { 𝐴 } ⊆ 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( 𝑥 = 𝐴 → 𝑥 ⊆ 𝐴 )
2		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
4	1 2 3	3imtr4i	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝒫 𝐴 )
5	4	ssriv	⊢ { 𝐴 } ⊆ 𝒫 𝐴