# 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}\in \mathrm{V}↔sngl{A}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 isset ${⊢}{A}\in \mathrm{V}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
2 pweq ${⊢}{x}={A}\to 𝒫{x}=𝒫{A}$
3 2 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to \exists {x}\phantom{\rule{.4em}{0ex}}𝒫{x}=𝒫{A}$
4 bj-snglss ${⊢}sngl{A}\subseteq 𝒫{A}$
5 sseq2 ${⊢}𝒫{x}=𝒫{A}\to \left(sngl{A}\subseteq 𝒫{x}↔sngl{A}\subseteq 𝒫{A}\right)$
6 4 5 mpbiri ${⊢}𝒫{x}=𝒫{A}\to sngl{A}\subseteq 𝒫{x}$
7 6 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}𝒫{x}=𝒫{A}\to \exists {x}\phantom{\rule{.4em}{0ex}}sngl{A}\subseteq 𝒫{x}$
8 vpwex ${⊢}𝒫{x}\in \mathrm{V}$
9 8 ssex ${⊢}sngl{A}\subseteq 𝒫{x}\to sngl{A}\in \mathrm{V}$
10 9 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}sngl{A}\subseteq 𝒫{x}\to sngl{A}\in \mathrm{V}$
11 3 7 10 3syl ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to sngl{A}\in \mathrm{V}$
12 1 11 sylbi ${⊢}{A}\in \mathrm{V}\to sngl{A}\in \mathrm{V}$
13 bj-snglinv ${⊢}{A}=\left\{{y}|\left\{{y}\right\}\in sngl{A}\right\}$
14 bj-snsetex ${⊢}sngl{A}\in \mathrm{V}\to \left\{{y}|\left\{{y}\right\}\in sngl{A}\right\}\in \mathrm{V}$
15 13 14 eqeltrid ${⊢}sngl{A}\in \mathrm{V}\to {A}\in \mathrm{V}$
16 12 15 impbii ${⊢}{A}\in \mathrm{V}↔sngl{A}\in \mathrm{V}$