This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex ⊢ { 𝑥 } ∈ 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 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )