Metamath Proof Explorer

Theorem bj-snglex

Description: A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snglex ⊢ A ∈ V ↔ sngl A ∈ V

Proof

Step Hyp Ref Expression
1 isset ⊢ A ∈ V ↔ ∃ x x = A
2 pweq ⊢ x = A → 𝒫 x = 𝒫 A
3 2 eximi ⊢ ∃ x x = A → ∃ x 𝒫 x = 𝒫 A
4 bj-snglss ⊢ sngl A ⊆ 𝒫 A
5 sseq2 ⊢ 𝒫 x = 𝒫 A → sngl A ⊆ 𝒫 x ↔ sngl A ⊆ 𝒫 A
6 4 5 mpbiri ⊢ 𝒫 x = 𝒫 A → sngl A ⊆ 𝒫 x
7 6 eximi ⊢ ∃ x 𝒫 x = 𝒫 A → ∃ x sngl A ⊆ 𝒫 x
8 vpwex ⊢ 𝒫 x ∈ V
9 8 ssex ⊢ sngl A ⊆ 𝒫 x → sngl A ∈ V
10 9 exlimiv ⊢ ∃ x sngl A ⊆ 𝒫 x → sngl A ∈ V
11 3 7 10 3syl ⊢ ∃ x x = A → sngl A ∈ V
12 1 11 sylbi ⊢ A ∈ V → sngl A ∈ V
13 bj-snglinv ⊢ A = y | y ∈ sngl A
14 bj-snsetex ⊢ sngl A ∈ V → y | y ∈ sngl A ∈ V
15 13 14 eqeltrid ⊢ sngl A ∈ V → A ∈ V
16 12 15 impbii ⊢ A ∈ V ↔ sngl A ∈ V