Theorem snelpw

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998)

	Ref	Expression
Hypothesis	snelpw.1	⊢ 𝐴 ∈ V
Assertion	snelpw	⊢ ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ∈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		snelpw.1	⊢ 𝐴 ∈ V
2	1	snss	⊢ ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ⊆ 𝐵 )
3		snex	⊢ { 𝐴 } ∈ V
4	3	elpw	⊢ ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 )
5	2 4	bitr4i	⊢ ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ∈ 𝒫 𝐵 )