Theorem snelsingles

Description: A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Hypothesis	snelsingles.1	⊢ 𝐴 ∈ V
Assertion	snelsingles	⊢ { 𝐴 } ∈ Singletons

Proof

Step	Hyp	Ref	Expression
1		snelsingles.1	⊢ 𝐴 ∈ V
2		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
3		eqcom	⊢ ( 𝑥 = 𝐴 ↔ 𝐴 = 𝑥 )
4	3	exbii	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 𝐴 = 𝑥 )
5	2 4	bitri	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝐴 = 𝑥 )
6	1 5	mpbi	⊢ ∃ 𝑥 𝐴 = 𝑥
7		sneq	⊢ ( 𝐴 = 𝑥 → { 𝐴 } = { 𝑥 } )
8	6 7	eximii	⊢ ∃ 𝑥 { 𝐴 } = { 𝑥 }
9		elsingles	⊢ ( { 𝐴 } ∈ Singletons ↔ ∃ 𝑥 { 𝐴 } = { 𝑥 } )
10	8 9	mpbir	⊢ { 𝐴 } ∈ Singletons