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 V \leftrightarrow sngl A \in V$

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

Metamath Proof Explorer