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

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 ⊢ A ∈ V → A ∈ B ↔ A ∈ 𝒫 B

Proof

Step Hyp Ref Expression
1 snssg ⊢ A ∈ V → A ∈ B ↔ A ⊆ B
2 snexg ⊢ A ∈ V → A ∈ V
3 elpwg ⊢ A ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
4 2 3 syl ⊢ A ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
5 1 4 bitr4d ⊢ A ∈ V → A ∈ B ↔ A ∈ 𝒫 B