Metamath Proof Explorer


Theorem snelpwg

Description: A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998) Put in closed form and avoid ax-nul . (Revised by BJ, 17-Jan-2025)

Ref Expression
Assertion snelpwg ( 𝐴𝑉 → ( 𝐴𝐵 ↔ { 𝐴 } ∈ 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 snssg ( 𝐴𝑉 → ( 𝐴𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )
2 snexg ( 𝐴𝑉 → { 𝐴 } ∈ V )
3 elpwg ( { 𝐴 } ∈ V → ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )
4 2 3 syl ( 𝐴𝑉 → ( { 𝐴 } ∈ 𝒫 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )
5 1 4 bitr4d ( 𝐴𝑉 → ( 𝐴𝐵 ↔ { 𝐴 } ∈ 𝒫 𝐵 ) )