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	⊢ ( 𝐴 ∈ V ↔ sngl 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
2		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
3	2	eximi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝒫 𝑥 = 𝒫 𝐴 )
4		bj-snglss	⊢ sngl 𝐴 ⊆ 𝒫 𝐴
5		sseq2	⊢ ( 𝒫 𝑥 = 𝒫 𝐴 → ( sngl 𝐴 ⊆ 𝒫 𝑥 ↔ sngl 𝐴 ⊆ 𝒫 𝐴 ) )
6	4 5	mpbiri	⊢ ( 𝒫 𝑥 = 𝒫 𝐴 → sngl 𝐴 ⊆ 𝒫 𝑥 )
7	6	eximi	⊢ ( ∃ 𝑥 𝒫 𝑥 = 𝒫 𝐴 → ∃ 𝑥 sngl 𝐴 ⊆ 𝒫 𝑥 )
8		vpwex	⊢ 𝒫 𝑥 ∈ V
9	8	ssex	⊢ ( sngl 𝐴 ⊆ 𝒫 𝑥 → sngl 𝐴 ∈ V )
10	9	exlimiv	⊢ ( ∃ 𝑥 sngl 𝐴 ⊆ 𝒫 𝑥 → sngl 𝐴 ∈ V )
11	3 7 10	3syl	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → sngl 𝐴 ∈ V )
12	1 11	sylbi	⊢ ( 𝐴 ∈ V → sngl 𝐴 ∈ V )
13		bj-snglinv	⊢ 𝐴 = { 𝑦 ∣ { 𝑦 } ∈ sngl 𝐴 }
14		bj-snsetex	⊢ ( sngl 𝐴 ∈ V → { 𝑦 ∣ { 𝑦 } ∈ sngl 𝐴 } ∈ V )
15	13 14	eqeltrid	⊢ ( sngl 𝐴 ∈ V → 𝐴 ∈ V )
16	12 15	impbii	⊢ ( 𝐴 ∈ V ↔ sngl 𝐴 ∈ V )