Theorem elsingles

Description: Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	elsingles	⊢ ( 𝐴 ∈ Singletons ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ Singletons → 𝐴 ∈ V )
2		snex	⊢ { 𝑥 } ∈ V
3		eleq1	⊢ ( 𝐴 = { 𝑥 } → ( 𝐴 ∈ V ↔ { 𝑥 } ∈ V ) )
4	2 3	mpbiri	⊢ ( 𝐴 = { 𝑥 } → 𝐴 ∈ V )
5	4	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 ∈ V )
6		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ Singletons ↔ 𝐴 ∈ Singletons ) )
7		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = { 𝑥 } ↔ 𝐴 = { 𝑥 } ) )
8	7	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 = { 𝑥 } ↔ ∃ 𝑥 𝐴 = { 𝑥 } ) )
9		df-singles	⊢ Singletons = ran Singleton
10	9	eleq2i	⊢ ( 𝑦 ∈ Singletons ↔ 𝑦 ∈ ran Singleton )
11		vex	⊢ 𝑦 ∈ V
12	11	elrn	⊢ ( 𝑦 ∈ ran Singleton ↔ ∃ 𝑥 𝑥 Singleton 𝑦 )
13		vex	⊢ 𝑥 ∈ V
14	13 11	brsingle	⊢ ( 𝑥 Singleton 𝑦 ↔ 𝑦 = { 𝑥 } )
15	14	exbii	⊢ ( ∃ 𝑥 𝑥 Singleton 𝑦 ↔ ∃ 𝑥 𝑦 = { 𝑥 } )
16	10 12 15	3bitri	⊢ ( 𝑦 ∈ Singletons ↔ ∃ 𝑥 𝑦 = { 𝑥 } )
17	6 8 16	vtoclbg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Singletons ↔ ∃ 𝑥 𝐴 = { 𝑥 } ) )
18	1 5 17	pm5.21nii	⊢ ( 𝐴 ∈ Singletons ↔ ∃ 𝑥 𝐴 = { 𝑥 } )